Let z be given.

Assume Hz.

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

Apply complex_I to the current goal.

Apply real_minus_SNo to the current goal.

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

Apply real_minus_SNo to the current goal.

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

∎