We will prove minus_SNo two_thirds = add_SNo (minus_SNo one_third) (minus_SNo one_third).
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) at position 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 H13S: SNo one_third.
An exact proof term for the current goal is (real_SNo one_third H13R).
An exact proof term for the current goal is (minus_add_SNo_distr one_third one_third H13S H13S).
∎