We will prove two_thirds = add_SNo 1 (minus_SNo one_third).
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 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).
An exact proof term for the current goal is add_one_third_two_thirds_eq_1.
rewrite the current goal using (add_SNo_minus_R2 two_thirds one_third H23S H13S) (from right to left) at position 1.
rewrite the current goal using Heq (from left to right) at position 1.
Use reflexivity.
∎