We will prove one_third < 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 H23R: two_thirds ∈ R.

An exact proof term for the current goal is two_thirds_in_R.

We prove the intermediate claim H13S: SNo one_third.

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

We prove the intermediate claim H23S: SNo two_thirds.

An exact proof term for the current goal is (real_SNo two_thirds H23R).

We prove the intermediate claim H23lt1: two_thirds < 1.

An exact proof term for the current goal is (RltE_lt two_thirds 1 Rlt_two_thirds_1).

An exact proof term for the current goal is (SNoLt_tra one_third two_thirds 1 H13S H23S SNo_1 one_third_lt_two_thirds H23lt1).

∎