Theorem: C03S04.aux (LeanInRome/S3_Logic/solutions/Solutions_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