no goals
ι : Type ?u.16670
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.16682
δ : Type ?u.16685
inst✝³ : Group α
inst✝² : AddCommSemigroup β
inst✝¹ : LE β
inst✝ : MulLEAddHomClass F α β
f : F
a b c : α
⊢ ↑f (a / c) ≤ ↑f (a / b) + ↑f (b / c)
simpa only [div_mul_div_cancel'] using map_mul_le_add f (a / b) (b / c)