k : Type u_2
E : Type u_1
PE : Type ?u.9072
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
ha : a < a'
hr : r < 1
⊢ (1 - r) • a + r • b < (1 - r) • a' + r • b
k : Type u_2
E : Type u_1
PE : Type ?u.9072
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
ha : a < a'
hr : r < 1
⊢ ↑(lineMap a b) r < ↑(lineMap a' b) r
simp only [lineMap_apply_module]
no goals
k : Type u_2
E : Type u_1
PE : Type ?u.9072
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
ha : a < a'
hr : r < 1
⊢ (1 - r) • a + r • b < (1 - r) • a' + r • b
exact add_lt_add_right (smul_lt_smul_of_pos ha (sub_pos.2 hr)) _