Let z be given.
Assume Hz.
Let w be given.
Assume Hw.
We will prove pa (add_SNo (mul_SNo (Re z) (Re w)) (minus_SNo (mul_SNo (Im w) (Im z)))) (add_SNo (mul_SNo (Im w) (Re z)) (mul_SNo (Im z) (Re w))) ∈ complex.
We prove the intermediate claim Lz0: Re z ∈ real.
An exact proof term for the current goal is complex_Re_real z Hz.
We prove the intermediate claim Lz1: Im z ∈ real.
An exact proof term for the current goal is complex_Im_real z Hz.
We prove the intermediate claim Lw0: Re w ∈ real.
An exact proof term for the current goal is complex_Re_real w Hw.
We prove the intermediate claim Lw1: Im w ∈ real.
An exact proof term for the current goal is complex_Im_real w Hw.
Apply complex_I to the current goal.
Apply real_add_SNo to the current goal.
Apply real_mul_SNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply real_minus_SNo to the current goal.
Apply real_mul_SNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply real_add_SNo to the current goal.
Apply real_mul_SNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply real_mul_SNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
∎