Let z be given.

Assume Hz.

Set s to be the term Re z ^ 2 + Im z ^ 2.

We prove the intermediate claim LRezR: SNo (Re z).

An exact proof term for the current goal is CSNo_ReR z Hz.

We prove the intermediate claim LImzR: SNo (Im z).

An exact proof term for the current goal is CSNo_ImR z Hz.

We prove the intermediate claim Ls: SNo s.

An exact proof term for the current goal is SNo_abs_sqr_CSNo z Hz.

We will prove CSNo (pa (Re z :/: s) (- (Im z :/: s))).

Apply CSNo_I to the current goal.

We will prove SNo (Re z :/: s).

Apply SNo_div_SNo to the current goal.

An exact proof term for the current goal is LRezR.

An exact proof term for the current goal is Ls.

We will prove SNo (- (Im z :/: s)).

Apply SNo_minus_SNo to the current goal.

Apply SNo_div_SNo to the current goal.

An exact proof term for the current goal is LImzR.

An exact proof term for the current goal is Ls.

∎