We will prove Rlt (minus_SNo 1) (minus_SNo two_thirds).
We prove the intermediate claim H23R: two_thirds ∈ R.
An exact proof term for the current goal is two_thirds_in_R.
We prove the intermediate claim Hm1R: minus_SNo 1 ∈ R.
An exact proof term for the current goal is (real_minus_SNo 1 real_1).
We prove the intermediate claim Hm23R: minus_SNo two_thirds ∈ R.
An exact proof term for the current goal is (real_minus_SNo two_thirds H23R).
We prove the intermediate claim Hle23: Rle two_thirds 1.
An exact proof term for the current goal is (Rlt_implies_Rle two_thirds 1 Rlt_two_thirds_1).
We prove the intermediate claim Hle: Rle (minus_SNo 1) (minus_SNo two_thirds).
An exact proof term for the current goal is (Rle_minus_contra two_thirds 1 Hle23).
We prove the intermediate claim Hneq: ¬ (minus_SNo 1 = minus_SNo two_thirds).
Assume Heq: minus_SNo 1 = minus_SNo two_thirds.
We prove the intermediate claim Heq1: 1 = two_thirds.
We prove the intermediate claim Htmp: minus_SNo (minus_SNo 1) = minus_SNo (minus_SNo two_thirds).
rewrite the current goal using Heq (from left to right).
Use reflexivity.
rewrite the current goal using (minus_SNo_minus_SNo_real 1 real_1) (from right to left) at position 1.
rewrite the current goal using (minus_SNo_minus_SNo_real two_thirds H23R) (from right to left).
An exact proof term for the current goal is Htmp.
We prove the intermediate claim H11: Rlt 1 1.
rewrite the current goal using Heq1 (from left to right) at position 1.
An exact proof term for the current goal is Rlt_two_thirds_1.
An exact proof term for the current goal is ((not_Rlt_sym 1 1 H11) H11).
An exact proof term for the current goal is (Rle_neq_implies_Rlt (minus_SNo 1) (minus_SNo two_thirds) Hle Hneq).
∎