An exact proof term for the current goal is (RltI 0 1 real_0 real_1 SNoLt_0_1).