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