We will prove Rle (minus_SNo two_thirds) 0.
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 H23S: SNo two_thirds.
An exact proof term for the current goal is (real_SNo two_thirds H23R).
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 H0lt13: Rlt 0 one_third.
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 H3non0: 3 ∉ {0}.
Assume H3in: 3 ∈ {0}.
We prove the intermediate claim H30: 3 = 0.
An exact proof term for the current goal is (SingE 0 3 H3in).
We prove the intermediate claim H3ne0: 3 ≠ 0.
We prove the intermediate claim H3def: 3 = ordsucc 2.
Use reflexivity.
rewrite the current goal using H3def (from left to right).
An exact proof term for the current goal is (neq_ordsucc_0 2).
An exact proof term for the current goal is (H3ne0 H30).
We prove the intermediate claim H3in: 3 ∈ ω ∖ {0}.
An exact proof term for the current goal is (setminusI ω {0} 3 H3omega H3non0).
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_pos 3 H3in).
We prove the intermediate claim H13S: SNo one_third.
An exact proof term for the current goal is (real_SNo one_third H13R).
We prove the intermediate claim Hlt13: 0 < one_third.
An exact proof term for the current goal is (RltE_lt 0 one_third H0lt13).
We prove the intermediate claim Hlt2: one_third < two_thirds.
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).
rewrite the current goal using (add_SNo_0R one_third H13S) (from right to left) at position 1.
An exact proof term for the current goal is (add_SNo_Lt2 one_third 0 one_third H13S SNo_0 H13S Hlt13).
We prove the intermediate claim Hpos: 0 < two_thirds.
An exact proof term for the current goal is (SNoLt_tra 0 one_third two_thirds SNo_0 H13S H23S Hlt13 Hlt2).
We prove the intermediate claim Hm23lt0: (minus_SNo two_thirds) < 0.
rewrite the current goal using minus_SNo_0 (from right to left) at position 1.
An exact proof term for the current goal is (minus_SNo_Lt_contra 0 two_thirds SNo_0 H23S Hpos).
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).
An exact proof term for the current goal is (Rlt_implies_Rle (minus_SNo two_thirds) 0 (RltI (minus_SNo two_thirds) 0 Hm23R real_0 Hm23lt0)).
∎