We will prove Rlt two_thirds 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 H0lt13: 0 < one_third.
An exact proof term for the current goal is one_third_pos.
We prove the intermediate claim Hlt: two_thirds < add_SNo two_thirds one_third.
rewrite the current goal using (add_SNo_0R two_thirds H23S) (from right to left) at position 1.
An exact proof term for the current goal is (add_SNo_Lt2 two_thirds 0 one_third H23S SNo_0 H13S H0lt13).
We prove the intermediate claim Heq: add_SNo two_thirds one_third = 1.
rewrite the current goal using (add_SNo_com two_thirds one_third H23S H13S) (from left to right) at position 1.
An exact proof term for the current goal is add_one_third_two_thirds_eq_1.
We prove the intermediate claim Hlt': two_thirds < 1.
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
An exact proof term for the current goal is (RltI two_thirds 1 H23R real_1 Hlt').
∎