We will prove add_SNo (minus_SNo 1) two_thirds = minus_SNo one_third.
We prove the intermediate claim H23eq: 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 H23eq (from left to right).
We prove the intermediate claim Hm1S: SNo (minus_SNo 1).
An exact proof term for the current goal is (SNo_minus_SNo 1 SNo_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).
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 Hassoc: add_SNo (minus_SNo 1) (add_SNo 1 (minus_SNo one_third)) = add_SNo (add_SNo (minus_SNo 1) 1) (minus_SNo one_third).
An exact proof term for the current goal is (add_SNo_assoc (minus_SNo 1) 1 (minus_SNo one_third) Hm1S SNo_1 Hm13S).
rewrite the current goal using Hassoc (from left to right).
We prove the intermediate claim Hinv: add_SNo (minus_SNo 1) 1 = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_linv 1 SNo_1).
rewrite the current goal using Hinv (from left to right).
An exact proof term for the current goal is (add_SNo_0L (minus_SNo one_third) Hm13S).
∎