Let a, b and r be given.
Assume HaR: a ∈ R.
Assume HbR: b ∈ R.
Assume HrR: r ∈ R.
Assume Hrlt1: Rlt r 1.
Assume Hlt: Rlt (R_bounded_distance a b) r.
Set t to be the term add_SNo a (minus_SNo b).
We prove the intermediate claim HmbR: minus_SNo b ∈ R.
An exact proof term for the current goal is (real_minus_SNo b HbR).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (real_add_SNo a HaR (minus_SNo b) HmbR).
We prove the intermediate claim HabsR: abs_SNo t ∈ R.
An exact proof term for the current goal is (abs_SNo_in_R t HtR).
We prove the intermediate claim Hbddef: R_bounded_distance a b = If_i (Rlt (abs_SNo t) 1) (abs_SNo t) 1.
Use reflexivity.
We prove the intermediate claim HIfRlt: Rlt (If_i (Rlt (abs_SNo t) 1) (abs_SNo t) 1) r.
rewrite the current goal using Hbddef (from right to left).
An exact proof term for the current goal is Hlt.
Apply (xm (Rlt (abs_SNo t) 1)) to the current goal.
Assume Hablt1: Rlt (abs_SNo t) 1.
We prove the intermediate claim HabRlt: Rlt (abs_SNo t) r.
rewrite the current goal using (If_i_1 (Rlt (abs_SNo t) 1) (abs_SNo t) 1 Hablt1) (from right to left).
An exact proof term for the current goal is HIfRlt.
An exact proof term for the current goal is (RltE_lt (abs_SNo t) r HabRlt).
Assume Hnablt1: ¬ (Rlt (abs_SNo t) 1).
We prove the intermediate claim H1lt: Rlt 1 r.
rewrite the current goal using (If_i_0 (Rlt (abs_SNo t) 1) (abs_SNo t) 1 Hnablt1) (from right to left).
An exact proof term for the current goal is HIfRlt.
We prove the intermediate claim Hrr: Rlt r r.
An exact proof term for the current goal is (Rlt_tra r 1 r Hrlt1 H1lt).
An exact proof term for the current goal is (FalseE ((not_Rlt_refl r HrR) Hrr) (abs_SNo t < r)).
∎