We will prove minus_SNo two_thirds = add_SNo (minus_SNo 1) 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 H13S: SNo one_third.
An exact proof term for the current goal is (real_SNo one_third H13R).
We prove the intermediate claim Hm13S: SNo (minus_SNo one_third).
An exact proof term for the current goal is (SNo_minus_SNo one_third H13S).
We prove the intermediate claim Heq: two_thirds = add_SNo 1 (minus_SNo one_third).
An exact proof term for the current goal is two_thirds_eq_1_minus_one_third.
rewrite the current goal using Heq (from left to right) at position 1.
rewrite the current goal using (minus_add_SNo_distr 1 (minus_SNo one_third) SNo_1 Hm13S) (from left to right) at position 1.
rewrite the current goal using (minus_SNo_minus_SNo_real one_third H13R) (from left to right) at position 1.
Use reflexivity.
∎