Theorem: C03S04.auxαα (MIL/C03_Logic/S04_Conjunction_and_Iff.lean)

State before:
x y : ℝ
h : x ^ 2 + y ^ 2 = 0
⊢ x ^ 2 = 0
Tactic:
linarith [pow_two_nonneg x, pow_two_nonneg y]
State after:
no goals