An exact proof term for the current goal is real_complex 0 real_0.