Let x be given.

Assume Hx.

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

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

An exact proof term for the current goal is complex_Im_eq 0 real_0 x Hx.

∎