We will prove pa 0 1 ∈ complex.

Apply complex_I to the current goal.

An exact proof term for the current goal is real_0.

An exact proof term for the current goal is real_1.

∎