calc
  a ^ 2 + 2 * a * b + b ^ 2 = (a + b) ^ 2 := by ring
  _ ≥ 0 := by apply pow_two_nonneg
case h
a b c d e : ℝ
⊢ 0 ≤ a ^ 2 + 2 * a * b + b ^ 2

a b c d e : ℝ
h : 0 ≤ a ^ 2 + 2 * a * b + b ^ 2
⊢ -(a * b) * 2 ≤ a ^ 2 + b ^ 2
a b c d e : ℝ
h : 0 ≤ a ^ 2 + 2 * a * b + b ^ 2
⊢ -(a * b) * 2 ≤ a ^ 2 + b ^ 2