Let z be given.
Assume Hz Hznz.
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.
Set u to be the term recip_SNo s.
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 Ls: SNo s.
An exact proof term for the current goal is SNo_abs_sqr_CSNo z Hz.
We prove the intermediate claim LsC: CSNo s.
An exact proof term for the current goal is SNo_CSNo s Ls.
We prove the intermediate claim Lu: SNo u.
An exact proof term for the current goal is SNo_recip_SNo s Ls.
We prove the intermediate claim LuC: CSNo u.
An exact proof term for the current goal is SNo_CSNo u Lu.
We prove the intermediate claim LReuS: SNo (Re u).
An exact proof term for the current goal is CSNo_ReR u LuC.
We prove the intermediate claim LImuS: SNo (Im u).
An exact proof term for the current goal is CSNo_ImR u LuC.
We prove the intermediate claim Luy: CSNo (u ⨯ y).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is LuC.
Apply SNo_CSNo to the current goal.
An exact proof term for the current goal is Ly.
We prove the intermediate claim Lsnz: s ≠ 0.
Assume H1: s = 0.
Apply Hznz to the current goal.
We will prove z = 0.
An exact proof term for the current goal is abs_sqr_CSNo_zero z Hz H1.
We prove the intermediate claim L1: Re (i ⨯ u ⨯ y) = 0.
rewrite the current goal using mul_CSNo_CRe i (u ⨯ y) CSNo_Complex_i ?? (from left to right).
We will prove Re i * Re (u ⨯ y) + - (Im (u ⨯ y) * Im i) = 0.
rewrite the current goal using Re_i (from left to right).
rewrite the current goal using Im_i (from left to right).
We will prove 0 * Re (u ⨯ y) + - (Im (u ⨯ y) * 1) = 0.
rewrite the current goal using mul_SNo_zeroL (Re (u ⨯ y)) (CSNo_ReR (u ⨯ y) (CSNo_mul_CSNo u y LuC (SNo_CSNo y Ly))) (from left to right).
rewrite the current goal using mul_SNo_oneR (Im (u ⨯ y)) (CSNo_ImR (u ⨯ y) (CSNo_mul_CSNo u y LuC (SNo_CSNo y Ly))) (from left to right).
We will prove 0 + - Im (u ⨯ y) = 0.
rewrite the current goal using mul_CSNo_CIm u y LuC (SNo_CSNo y Ly) (from left to right).
We will prove 0 + - (Im y * Re u + Im u * Re y) = 0.
rewrite the current goal using SNo_Im y Ly (from left to right).
rewrite the current goal using SNo_Im u Lu (from left to right).
We will prove 0 + - (0 * Re u + 0 * Re y) = 0.
rewrite the current goal using mul_SNo_zeroL (Re u) LReuS (from left to right).
rewrite the current goal using mul_SNo_zeroL (Re y) (CSNo_ReR y (SNo_CSNo y Ly)) (from left to right).
We will prove 0 + - (0 + 0) = 0.
rewrite the current goal using add_SNo_0L 0 SNo_0 (from left to right).
rewrite the current goal using minus_SNo_0 (from left to right).
An exact proof term for the current goal is add_SNo_0L 0 SNo_0.
We prove the intermediate claim L2: Im (i ⨯ u ⨯ y) = u * y.
rewrite the current goal using mul_CSNo_CIm i (u ⨯ y) CSNo_Complex_i ?? (from left to right).
We will prove Im (u ⨯ y) * Re i + Im i * Re (u ⨯ y) = u * y.
rewrite the current goal using Re_i (from left to right).
rewrite the current goal using Im_i (from left to right).
We will prove Im (u ⨯ y) * 0 + 1 * Re (u ⨯ y) = u * y.
rewrite the current goal using mul_SNo_zeroR (Im (u ⨯ y)) (CSNo_ImR (u ⨯ y) (CSNo_mul_CSNo u y LuC (SNo_CSNo y Ly))) (from left to right).
rewrite the current goal using mul_SNo_oneL (Re (u ⨯ y)) (CSNo_ReR (u ⨯ y) (CSNo_mul_CSNo u y LuC (SNo_CSNo y Ly))) (from left to right).
We will prove 0 + Re (u ⨯ y) = u * y.
rewrite the current goal using mul_CSNo_mul_SNo u y Lu Ly (from left to right).
rewrite the current goal using SNo_Re (u * y) (SNo_mul_SNo u y ?? ??) (from left to right).
We will prove 0 + u * y = u * y.
An exact proof term for the current goal is add_SNo_0L (u * y) (SNo_mul_SNo u y ?? ??).
We will prove z ⨯ pa (x :/: s) (- (y :/: s)) = 1.
Use transitivity with and (z ⨯ (u ⨯ x + :-: i ⨯ u ⨯ y)).
We will prove z ⨯ pa (x :/: s) (- (y :/: s)) = z ⨯ (u ⨯ x + :-: i ⨯ u ⨯ y).
Use f_equal.
We will prove pa (x :/: s) (- (y :/: s)) = u ⨯ x + :-: i ⨯ u ⨯ y.
Apply CSNo_ReIm_split (pa (x :/: s) (- (y :/: s))) (u ⨯ x + :-: i ⨯ u ⨯ y) to the current goal.
We will prove CSNo (pa (x :/: s) (- (y :/: s))).
Apply CSNo_I to the current goal.
We will prove SNo (x :/: s).
An exact proof term for the current goal is SNo_div_SNo x s ?? ??.
Apply SNo_minus_SNo to the current goal.
We will prove SNo (y :/: s).
An exact proof term for the current goal is SNo_div_SNo y s ?? ??.
We will prove CSNo (u ⨯ x + :-: i ⨯ u ⨯ y).
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is CSNo_mul_CSNo u x LuC (SNo_CSNo x Lx).
Apply CSNo_minus_CSNo to the current goal.
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is CSNo_Complex_i.
An exact proof term for the current goal is CSNo_mul_CSNo u y LuC (SNo_CSNo y Ly).
We will prove Re (pa (x :/: s) (- (y :/: s))) = Re (u ⨯ x + :-: i ⨯ u ⨯ y).
rewrite the current goal using CSNo_Re2 (x :/: s) (- (y :/: s)) (SNo_div_SNo x s Lx Ls) (SNo_minus_SNo (y :/: s) (SNo_div_SNo y s Ly Ls)) (from left to right).
We will prove x :/: s = Re (u ⨯ x + :-: i ⨯ u ⨯ y).
rewrite the current goal using add_CSNo_CRe (u ⨯ x) (:-: i ⨯ u ⨯ y) (CSNo_mul_CSNo u x LuC (SNo_CSNo x Lx)) (CSNo_minus_CSNo (i ⨯ u ⨯ y) (CSNo_mul_CSNo i (u ⨯ y) CSNo_Complex_i (CSNo_mul_CSNo u y LuC (SNo_CSNo y Ly)))) (from left to right).
We will prove x :/: s = Re (u ⨯ x) + Re (:-: i ⨯ u ⨯ y).
rewrite the current goal using mul_CSNo_mul_SNo u x Lu Lx (from left to right).
We will prove x :/: s = Re (u * x) + Re (:-: i ⨯ u ⨯ y).
rewrite the current goal using SNo_Re (u * x) (SNo_mul_SNo u x ?? ??) (from left to right).
We will prove x :/: s = u * x + Re (:-: i ⨯ u ⨯ y).
rewrite the current goal using minus_CSNo_CRe (i ⨯ u ⨯ y) (CSNo_mul_CSNo i (u ⨯ y) CSNo_Complex_i (CSNo_mul_CSNo u y LuC (SNo_CSNo y Ly))) (from left to right).
We will prove x :/: s = u * x + - Re (i ⨯ u ⨯ y).
rewrite the current goal using L1 (from left to right).
We will prove x :/: s = u * x + - 0.
rewrite the current goal using minus_SNo_0 (from left to right).
We will prove x :/: s = u * x + 0.
rewrite the current goal using add_SNo_0R (u * x) (SNo_mul_SNo u x ?? ??) (from left to right).
We will prove x * u = u * x.
An exact proof term for the current goal is mul_SNo_com x u ?? ??.
We will prove Im (pa (x :/: s) (- (y :/: s))) = Im (u ⨯ x + :-: i ⨯ u ⨯ y).
rewrite the current goal using CSNo_Im2 (x :/: s) (- (y :/: s)) (SNo_div_SNo x s Lx Ls) (SNo_minus_SNo (y :/: s) (SNo_div_SNo y s Ly Ls)) (from left to right).
rewrite the current goal using add_CSNo_CIm (u ⨯ x) (:-: i ⨯ u ⨯ y) (CSNo_mul_CSNo u x LuC (SNo_CSNo x Lx)) (CSNo_minus_CSNo (i ⨯ u ⨯ y) (CSNo_mul_CSNo i (u ⨯ y) CSNo_Complex_i (CSNo_mul_CSNo u y LuC (SNo_CSNo y Ly)))) (from left to right).
We will prove - (y :/: s) = Im (u ⨯ x) + Im (:-: i ⨯ u ⨯ y).
rewrite the current goal using minus_CSNo_CIm (i ⨯ u ⨯ y) (CSNo_mul_CSNo i (u ⨯ y) CSNo_Complex_i (CSNo_mul_CSNo u y LuC (SNo_CSNo y Ly))) (from left to right).
We will prove - (y :/: s) = Im (u ⨯ x) + - Im (i ⨯ u ⨯ y).
rewrite the current goal using mul_CSNo_mul_SNo u x Lu Lx (from left to right).
rewrite the current goal using SNo_Im (u * x) (SNo_mul_SNo u x ?? ??) (from left to right).
We will prove - (y :/: s) = 0 + - Im (i ⨯ u ⨯ y).
rewrite the current goal using L2 (from left to right).
We will prove - (y :/: s) = 0 + - (u * y).
We will prove - (y * u) = 0 + - (u * y).
rewrite the current goal using add_SNo_0L (- u * y) (SNo_minus_SNo (u * y) (SNo_mul_SNo u y ?? ??)) (from left to right).
Use f_equal.
An exact proof term for the current goal is mul_SNo_com y u ?? ??.
We will prove z ⨯ (u ⨯ x + :-: i ⨯ u ⨯ y) = 1.
Apply CSNo_relative_recip z Hz u Lu to the current goal.
We will prove (x ^ 2 + y ^ 2) * u = 1.
We will prove s * u = 1.
An exact proof term for the current goal is recip_SNo_invR s Ls Lsnz.
∎