no goals
k : Type u_1
E : Type u_2
PE : Type ?u.93916
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a b : E
r r' : k
h : 0 < r
⊢ a ≤ ↑(lineMap a b) r ↔ ↑(lineMap a b) 0 ≤ ↑(lineMap a b) r
rw [lineMap_apply_zero]