We will prove two_thirds ∈ R.

We prove the intermediate claim Hdef: two_thirds = add_SNo one_third one_third.

Use reflexivity.

rewrite the current goal using Hdef (from left to right).

We prove the intermediate claim H13R: one_third ∈ R.

An exact proof term for the current goal is one_third_in_R.

An exact proof term for the current goal is (real_add_SNo one_third H13R one_third H13R).

∎