β : Type ?u.245753
A : Type ?u.245756
G : Type ?u.245759
M : Type ?u.245762
R : Type u_1
inst✝ : LinearOrderedSemiring R
a b : R
hb : 0 ≤ b
⊢ a ^ 2 < b ^ 2 → a < b
β : Type ?u.245753
A : Type ?u.245756
G : Type ?u.245759
M : Type ?u.245762
R : Type u_1
inst✝ : LinearOrderedSemiring R
a b : R
hb : 0 ≤ b
⊢ a * a < b * b → a < b
simp_rw [← sq]
no goals
β : Type ?u.245753
A : Type ?u.245756
G : Type ?u.245759
M : Type ?u.245762
R : Type u_1
inst✝ : LinearOrderedSemiring R
a b : R
hb : 0 ≤ b
⊢ a ^ 2 < b ^ 2 → a < b
exact lt_of_pow_lt_pow _ hb