Let z be given.
Assume Hz.
We will
prove SNo (Re z ^ 2 + Im z ^ 2).
Apply SNo_add_SNo to the current goal.
Apply SNo_exp_SNo_nat to the current goal.
An
exact proof term for the current goal is
CSNo_ReR z Hz.
An exact proof term for the current goal is nat_2.
Apply SNo_exp_SNo_nat to the current goal.
An
exact proof term for the current goal is
CSNo_ImR z Hz.
An exact proof term for the current goal is nat_2.