no goals
ι : Type ?u.114417
α : Type u_2
β✝ : Type ?u.114423
inst✝¹ : LinearOrderedSemifield α
a b c✝ d e : α
m n : ℤ
β : Type u_1
inst✝ : Preorder β
f : β → α
hf : StrictMono f
c : α
hc : 0 < c
⊢ StrictMono fun x => f x / c
simpa only [div_eq_mul_inv] using hf.mul_const (inv_pos.2 hc)