Let z be given.

Assume Hz.

Apply complex_E z Hz to the current goal.

Let x be given.

Assume Hx.

Let y be given.

Assume Hy Hzxy.

rewrite the current goal using Hzxy (from left to right).

rewrite the current goal using complex_Re_eq x Hx y Hy (from left to right).

rewrite the current goal using complex_Im_eq x Hx y Hy (from left to right).

We will prove pa x y = x + i * y.

We will prove pa x y = pa (add_SNo (Re x) (Re (i * y))) (add_SNo (Im x) (Im (i * y))).

rewrite the current goal using real_Re_eq x Hx (from left to right).

rewrite the current goal using real_Im_eq x Hx (from left to right).

rewrite the current goal using real_Re_i_eq y Hy (from left to right).

rewrite the current goal using real_Im_i_eq y Hy (from left to right).

We will prove pa x y = pa (add_SNo x 0) (add_SNo 0 y).

rewrite the current goal using add_SNo_0R x (real_SNo x Hx) (from left to right).

rewrite the current goal using add_SNo_0L y (real_SNo y Hy) (from left to right).

Use reflexivity.

∎