We will prove add_SNo one_third two_thirds = 1.
We prove the intermediate claim H3S: SNo 3.
An exact proof term for the current goal is (real_SNo 3 real_3).
We prove the intermediate claim HrS: SNo (recip_SNo 3).
An exact proof term for the current goal is (SNo_recip_SNo 3 H3S).
We prove the intermediate claim Hdiv1: div_SNo 1 3 = mul_SNo 1 (recip_SNo 3).
Use reflexivity.
We prove the intermediate claim Hdiv2: div_SNo 2 3 = mul_SNo 2 (recip_SNo 3).
Use reflexivity.
rewrite the current goal using one_third_eq_div_1_3 (from left to right) at position 1.
rewrite the current goal using two_thirds_eq_div_2_3 (from left to right) at position 1.
rewrite the current goal using Hdiv1 (from left to right) at position 1.
rewrite the current goal using Hdiv2 (from left to right) at position 1.
rewrite the current goal using (mul_SNo_distrR 1 2 (recip_SNo 3) SNo_1 SNo_2 HrS) (from right to left) at position 1.
We prove the intermediate claim H12eq: add_SNo 1 2 = 3.
rewrite the current goal using (add_SNo_com 1 2 SNo_1 SNo_2) (from left to right).
rewrite the current goal using add_SNo_2_1_eq_3 (from right to left).
Use reflexivity.
rewrite the current goal using H12eq (from left to right) at position 1.
We prove the intermediate claim H3ne0: 3 ≠ 0.
We prove the intermediate claim H3def: 3 = ordsucc 2.
Use reflexivity.
rewrite the current goal using H3def (from left to right).
An exact proof term for the current goal is (neq_ordsucc_0 2).
An exact proof term for the current goal is (recip_SNo_invR 3 H3S H3ne0).
∎