no goals
k : Type u_1
E : Type u_2
PE : Type ?u.200700
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
f : k → E
a b r : k
hab : a < b
h₀ : 0 < r
h₁ : r < 1
⊢ f (↑(lineMap a b) r) ≤ ↑(lineMap (f a) (f b)) r ↔ slope f a (↑(lineMap a b) r) ≤ slope f (↑(lineMap a b) r) b
rw [map_le_lineMap_iff_slope_le_slope_left (mul_pos h₀ (sub_pos.2 hab)), ←
  lineMap_slope_lineMap_slope_lineMap f a b r, right_le_lineMap_iff_le h₁]