Let z be given.

Assume Hz.

Let w be given.

Assume Hw.

We will prove pa (add_SNo (Re z) (Re w)) (add_SNo (Im z) (Im w)) ∈ complex.

Apply complex_I to the current goal.

Apply real_add_SNo to the current goal.

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

An exact proof term for the current goal is complex_Re_real w Hw.

Apply real_add_SNo to the current goal.

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

An exact proof term for the current goal is complex_Im_real w Hw.

∎