β : Type ?u.233772
A : Type ?u.233775
G : Type ?u.233778
M : Type ?u.233781
R : Type u_1
inst✝ : StrictOrderedSemiring R
a x y : R
n m : ℕ
ha : 0 < a
⊢ 0 < a * a
β : Type ?u.233772
A : Type ?u.233775
G : Type ?u.233778
M : Type ?u.233781
R : Type u_1
inst✝ : StrictOrderedSemiring R
a x y : R
n m : ℕ
ha : 0 < a
⊢ 0 < a ^ 2
rw [sq]
no goals
β : Type ?u.233772
A : Type ?u.233775
G : Type ?u.233778
M : Type ?u.233781
R : Type u_1
inst✝ : StrictOrderedSemiring R
a x y : R
n m : ℕ
ha : 0 < a
⊢ 0 < a * a
exact mul_pos ha ha