An exact proof term for the current goal is (rational_numbers_Subq_R q Hq).