An exact proof term for the current goal is real_complex 1 real_1.