Let t and s be given.
Assume HtR: t ∈ R.
Assume HsR: s ∈ R.
Assume Hts: t ≤ s.
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim HsS: SNo s.
An exact proof term for the current goal is (real_SNo s HsR).
Apply (xm (Rlt t 1)) to the current goal.
Assume Htlt: Rlt t 1.
We prove the intermediate claim HtltS: t < 1.
An exact proof term for the current goal is (RltE_lt t 1 Htlt).
rewrite the current goal using (If_i_1 (Rlt t 1) t 1 Htlt) (from left to right).
Apply (xm (Rlt s 1)) to the current goal.
Assume Hslt: Rlt s 1.
rewrite the current goal using (If_i_1 (Rlt s 1) s 1 Hslt) (from left to right).
An exact proof term for the current goal is Hts.
Assume Hnsl: ¬ (Rlt s 1).
rewrite the current goal using (If_i_0 (Rlt s 1) s 1 Hnsl) (from left to right).
An exact proof term for the current goal is (SNoLtLe t 1 HtltS).
Assume Hntl: ¬ (Rlt t 1).
rewrite the current goal using (If_i_0 (Rlt t 1) t 1 Hntl) (from left to right).
Apply (xm (Rlt s 1)) to the current goal.
Assume Hslt: Rlt s 1.
rewrite the current goal using (If_i_1 (Rlt s 1) s 1 Hslt) (from left to right).
We prove the intermediate claim HsltS: s < 1.
An exact proof term for the current goal is (RltE_lt s 1 Hslt).
We prove the intermediate claim Ht1: t < 1.
An exact proof term for the current goal is (SNoLeLt_tra t s 1 HtS HsS SNo_1 Hts HsltS).
We prove the intermediate claim Htlt: Rlt t 1.
An exact proof term for the current goal is (RltI t 1 HtR real_1 Ht1).
An exact proof term for the current goal is (FalseE (Hntl Htlt) (1 ≤ s)).
Assume Hnsl: ¬ (Rlt s 1).
rewrite the current goal using (If_i_0 (Rlt s 1) s 1 Hnsl) (from left to right).
An exact proof term for the current goal is (SNoLe_ref 1).
∎