Let z be given.
Assume Hz.
Set x to be the term Re z.
Set y to be the term Im z.
Set s to be the term x ^ 2 + y ^ 2.
Assume H1: s = 0.
We prove the intermediate claim Lx: SNo x.
An exact proof term for the current goal is CSNo_ReR z Hz.
We prove the intermediate claim Ly: SNo y.
An exact proof term for the current goal is CSNo_ImR z Hz.
We prove the intermediate claim Lxx: SNo (x ^ 2).
An exact proof term for the current goal is SNo_exp_SNo_nat x Lx 2 nat_2.
We prove the intermediate claim Lyy: SNo (y ^ 2).
An exact proof term for the current goal is SNo_exp_SNo_nat y Ly 2 nat_2.
We prove the intermediate claim Ls: SNo s.
An exact proof term for the current goal is SNo_add_SNo (x ^ 2) (y ^ 2) Lxx Lyy.
We will prove z = 0.
Apply CSNo_ReIm_split z 0 Hz CSNo_0 to the current goal.
We will prove Re z = Re 0.
rewrite the current goal using Re_0 (from left to right).
We will prove x = 0.
Apply SNo_zero_or_sqr_pos' x Lx to the current goal.
Assume H2: x = 0.
An exact proof term for the current goal is H2.
Assume H2: 0 < x ^ 2.
We will prove False.
Apply SNoLt_irref 0 to the current goal.
We will prove 0 < 0.
rewrite the current goal using H1 (from right to left) at position 2.
We will prove 0 < s.
Apply SNoLtLe_tra 0 (x ^ 2) s SNo_0 ?? ?? H2 to the current goal.
We will prove x ^ 2 ≤ s.
rewrite the current goal using add_SNo_0R (x ^ 2) ?? (from right to left) at position 1.
We will prove x ^ 2 + 0 ≤ s.
Apply add_SNo_Le2 (x ^ 2) 0 (y ^ 2) ?? SNo_0 ?? to the current goal.
We will prove 0 ≤ y ^ 2.
Apply SNo_sqr_nonneg' y Ly to the current goal.
We will prove Im z = Im 0.
rewrite the current goal using Im_0 (from left to right).
We will prove y = 0.
Apply SNo_zero_or_sqr_pos' y Ly to the current goal.
Assume H2: y = 0.
An exact proof term for the current goal is H2.
Assume H2: 0 < y ^ 2.
We will prove False.
Apply SNoLt_irref 0 to the current goal.
We will prove 0 < 0.
rewrite the current goal using H1 (from right to left) at position 2.
We will prove 0 < s.
Apply SNoLtLe_tra 0 (y ^ 2) s SNo_0 ?? ?? H2 to the current goal.
We will prove y ^ 2 ≤ s.
rewrite the current goal using add_SNo_0L (y ^ 2) ?? (from right to left) at position 1.
We will prove 0 + y ^ 2 ≤ s.
Apply add_SNo_Le1 0 (y ^ 2) (x ^ 2) SNo_0 ?? ?? to the current goal.
We will prove 0 ≤ x ^ 2.
Apply SNo_sqr_nonneg' x Lx to the current goal.
∎