Let a and b be given.
Assume HaR: a ∈ R.
Assume HbR: b ∈ R.
We prove the intermediate claim HbM: minus_SNo b ∈ R.
An exact proof term for the current goal is (real_minus_SNo b HbR).
Set t to be the term add_SNo a (minus_SNo b).
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) HbM).
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 HabsNN: 0 ≤ abs_SNo t.
An exact proof term for the current goal is (abs_SNo_nonneg t HtS).
We prove the intermediate claim Hdef: R_bounded_distance a b = If_i (Rlt (abs_SNo t) 1) (abs_SNo t) 1.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
Apply (xm (Rlt (abs_SNo t) 1) (0 ≤ If_i (Rlt (abs_SNo t) 1) (abs_SNo t) 1)) to the current goal.
Assume Hlt: Rlt (abs_SNo t) 1.
rewrite the current goal using (If_i_1 (Rlt (abs_SNo t) 1) (abs_SNo t) 1 Hlt) (from left to right).
An exact proof term for the current goal is HabsNN.
Assume Hnlt: ¬ (Rlt (abs_SNo t) 1).
rewrite the current goal using (If_i_0 (Rlt (abs_SNo t) 1) (abs_SNo t) 1 Hnlt) (from left to right).
An exact proof term for the current goal is (SNoLtLe 0 1 SNoLt_0_1).
∎