We will prove Rlt (minus_SNo 1) (minus_SNo one_third).

We prove the intermediate claim Hm1R: minus_SNo 1 ∈ R.

An exact proof term for the current goal is (real_minus_SNo 1 real_1).

We prove the intermediate claim H13R: one_third ∈ R.

An exact proof term for the current goal is one_third_in_R.

We prove the intermediate claim Hm13R: minus_SNo one_third ∈ R.

An exact proof term for the current goal is (real_minus_SNo one_third H13R).

An exact proof term for the current goal is (RltI (minus_SNo 1) (minus_SNo one_third) Hm1R Hm13R minus_1_lt_minus_one_third_SNo).

∎