We will prove one_third = div_SNo 1 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 Hdiv: div_SNo 1 3 = inv_nat 3.
An exact proof term for the current goal is (div_SNo_1_eq_inv_nat 3 H3S).
We prove the intermediate claim Hdef: one_third = inv_nat 3.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using Hdiv (from right to left).
Use reflexivity.
∎