We will prove one_third ∈ R.
We prove the intermediate claim H3nat: nat_p 3.
An exact proof term for the current goal is (nat_ordsucc 2 nat_2).
We prove the intermediate claim H3omega: 3 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 3 H3nat).
We prove the intermediate claim Hdef: one_third = inv_nat 3.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (inv_nat_real 3 H3omega).
∎