ι : Type ?u.113111
α : Type u_2
β✝ : Type ?u.113117
inst✝¹ : LinearOrderedSemifield α
a b c✝ d e : α
m n : ℤ
β : Type u_1
inst✝ : Preorder β
f : β → α
hf : Monotone f
c : α
hc : 0 ≤ c
this : DecidableRel fun x x_1 => x ≤ x_1
⊢ Monotone fun x => f x / c
ι : Type ?u.113111
α : Type u_2
β✝ : Type ?u.113117
inst✝¹ : LinearOrderedSemifield α
a b c✝ d e : α
m n : ℤ
β : Type u_1
inst✝ : Preorder β
f : β → α
hf : Monotone f
c : α
hc : 0 ≤ c
⊢ Monotone fun x => f x / c
haveI := @LinearOrder.decidableLE α _
no goals
ι : Type ?u.113111
α : Type u_2
β✝ : Type ?u.113117
inst✝¹ : LinearOrderedSemifield α
a b c✝ d e : α
m n : ℤ
β : Type u_1
inst✝ : Preorder β
f : β → α
hf : Monotone f
c : α
hc : 0 ≤ c
this : DecidableRel fun x x_1 => x ≤ x_1
⊢ Monotone fun x => f x / c
simpa only [div_eq_mul_inv] using (monotone_mul_right_of_nonneg (inv_nonneg.2 hc)).comp hf