We will prove two_thirds = div_SNo 2 3.
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.
We prove the intermediate claim Hdef23: two_thirds = add_SNo one_third one_third.
Use reflexivity.
rewrite the current goal using Hdef23 (from left to right).
rewrite the current goal using one_third_eq_div_1_3 (from left to right).
rewrite the current goal using Hdiv1 (from left to right).
rewrite the current goal using Hdiv2 (from left to right).
rewrite the current goal using (mul_SNo_oneL (recip_SNo 3) HrS) (from left to right).
We prove the intermediate claim H2mul: mul_SNo (add_SNo 1 1) (recip_SNo 3) = mul_SNo 2 (recip_SNo 3).
rewrite the current goal using add_SNo_1_1_2 (from left to right).
Use reflexivity.
rewrite the current goal using H2mul (from right to left) at position 1.
rewrite the current goal using (mul_SNo_distrR 1 1 (recip_SNo 3) SNo_1 SNo_1 HrS) (from left to right) at position 1.
rewrite the current goal using (mul_SNo_oneL (recip_SNo 3) HrS) (from left to right).
Use reflexivity.
∎