R : Type u_1
A : Type u_2
a✝ b✝ : A
r : R
inst✝³ : OrderedCommRing R
inst✝² : OrderedRing A
inst✝¹ : Algebra R A
inst✝ : OrderedSMul R A
a b : R
h : a ≤ b
⊢ 0 ≤ (b - a) • 1
R : Type u_1
A : Type u_2
a✝ b✝ : A
r : R
inst✝³ : OrderedCommRing R
inst✝² : OrderedRing A
inst✝¹ : Algebra R A
inst✝ : OrderedSMul R A
a b : R
h : a ≤ b
⊢ ↑(algebraMap R A) a ≤ ↑(algebraMap R A) b
rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, ← sub_nonneg, ← sub_smul]
R : Type u_1
A : Type u_2
a✝ b✝ : A
r : R
inst✝³ : OrderedCommRing R
inst✝² : OrderedRing A
inst✝¹ : Algebra R A
inst✝ : OrderedSMul R A
a b : R
h : a ≤ b
⊢ 0 ≤ (b - a) • 0

R : Type u_1
A : Type u_2
a✝ b✝ : A
r : R
inst✝³ : OrderedCommRing R
inst✝² : OrderedRing A
inst✝¹ : Algebra R A
inst✝ : OrderedSMul R A
a b : R
h : a ≤ b
⊢ (b - a) • 0 ≤ (b - a) • 1
R : Type u_1
A : Type u_2
a✝ b✝ : A
r : R
inst✝³ : OrderedCommRing R
inst✝² : OrderedRing A
inst✝¹ : Algebra R A
inst✝ : OrderedSMul R A
a b : R
h : a ≤ b
⊢ 0 ≤ (b - a) • 1
trans (b - a) • (0 : A)
no goals
R : Type u_1
A : Type u_2
a✝ b✝ : A
r : R
inst✝³ : OrderedCommRing R
inst✝² : OrderedRing A
inst✝¹ : Algebra R A
inst✝ : OrderedSMul R A
a b : R
h : a ≤ b
⊢ 0 ≤ (b - a) • 0
simp
no goals
R : Type u_1
A : Type u_2
a✝ b✝ : A
r : R
inst✝³ : OrderedCommRing R
inst✝² : OrderedRing A
inst✝¹ : Algebra R A
inst✝ : OrderedSMul R A
a b : R
h : a ≤ b
⊢ (b - a) • 0 ≤ (b - a) • 1
exact smul_le_smul_of_nonneg zero_le_one (sub_nonneg.mpr h)