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