no goals
ι : Type ?u.23876
α : Type u_1
β : Type ?u.23882
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hb : 0 < b
h : a / b ≤ c
⊢ a = a / b * b
rw [div_mul_cancel _ (ne_of_lt hb).symm]
no goals
ι : Type ?u.23876
α : Type u_1
β : Type ?u.23882
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hb : 0 < b
h : a ≤ c * b
⊢ c * b / b = c
refine' (div_eq_iff (ne_of_gt hb)).mpr rfl