Let x be given.

Assume Hx.

We will prove pa (add_SNo (mul_SNo (Re (pa 0 1)) (Re x)) (minus_SNo (mul_SNo (Im x) (Im (pa 0 1))))) (add_SNo (mul_SNo (Im x) (Re (pa 0 1))) (mul_SNo (Im (pa 0 1)) (Re x))) = pa 0 x.

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 complex_Re_eq 0 real_0 1 real_1 (from left to right).

rewrite the current goal using complex_Im_eq 0 real_0 1 real_1 (from left to right).

We will prove pa (add_SNo (mul_SNo 0 x) (minus_SNo (mul_SNo 0 1))) (add_SNo (mul_SNo 0 0) (mul_SNo 1 x)) = pa 0 x.

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

rewrite the current goal using mul_SNo_zeroL 1 SNo_1 (from left to right).

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

rewrite the current goal using mul_SNo_zeroL 0 SNo_0 (from left to right).

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

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

rewrite the current goal using add_SNo_0L 0 SNo_0 (from left to right).

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

Use reflexivity.

∎