We will prove 0 < two_thirds.

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 H13S: SNo one_third.

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

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 H23S: SNo two_thirds.

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

We prove the intermediate claim Hlt13: 0 < one_third.

An exact proof term for the current goal is one_third_pos.

We prove the intermediate claim H1lt2: one_third < two_thirds.

We prove the intermediate claim Hdef: two_thirds = add_SNo one_third one_third.

Use reflexivity.

rewrite the current goal using Hdef (from left to right).

rewrite the current goal using (add_SNo_0R one_third H13S) (from right to left) at position 1.

An exact proof term for the current goal is (add_SNo_Lt2 one_third 0 one_third H13S SNo_0 H13S Hlt13).

An exact proof term for the current goal is (SNoLt_tra 0 one_third two_thirds SNo_0 H13S H23S Hlt13 H1lt2).

∎