no goals
k : Type u_1
E : Type u_2
PE : Type ?u.72601
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b 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]