Let z be given.
Assume Hz.
Set x to be the term Re z.
Set y to be the term Im z.
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 will
prove 0 ≤ x ^ 2 + y ^ 2.
rewrite the current goal using add_SNo_0L 0 SNo_0 (from right to left) at position 1.
We will
prove 0 + 0 ≤ x ^ 2 + y ^ 2.
Apply add_SNo_Le3 0 0 (x ^ 2) (y ^ 2) SNo_0 SNo_0 Lxx Lyy to the current goal.
rewrite the current goal using exp_SNo_nat_2 x Lx (from left to right).
An exact proof term for the current goal is SNo_sqr_nonneg x Lx.
rewrite the current goal using exp_SNo_nat_2 y Ly (from left to right).
An exact proof term for the current goal is SNo_sqr_nonneg y Ly.