An exact proof term for the current goal is (Subq_rational_real).