What tactic do I use to show squares are non-negative?

Stream: new members

[YH]

I want to do

lemma sq_geq_zero (a : ℝ) : (a ^ 2 ≥ 0) := sorry

as an exercise, but I don't know any tactic for this.
(or is there a way to cases a as either positive, negative or zero?)

[Johan Commelin]

There is the lemma le_total a 0

[Johan Commelin]

@YH You could do cases on that

[Johan Commelin]

Or the tactic by_cases h : a ≥ 0

[Johan Commelin]

@YH You could do cases on that