We will prove Rlt one_third 1.

An exact proof term for the current goal is (RltI one_third 1 one_third_in_R real_1 one_third_lt_1_SNo).

∎