We will prove (minus_SNo 1) < (minus_SNo one_third).
We prove the intermediate claim H13R: one_third ∈ R.
An exact proof term for the current goal is one_third_in_R.
We prove the intermediate claim H13S: SNo one_third.
An exact proof term for the current goal is (real_SNo one_third H13R).
An exact proof term for the current goal is (minus_SNo_Lt_contra one_third 1 H13S SNo_1 one_third_lt_1_SNo).
∎