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 Habslt: abs_SNo (add_SNo a (minus_SNo b)) < r.
We will prove 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 HabRlt: Rlt (abs_SNo t) r.
An exact proof term for the current goal is (RltI (abs_SNo t) r HabsR HrR Habslt).
We prove the intermediate claim Hablt1: Rlt (abs_SNo t) 1.
An exact proof term for the current goal is (Rlt_tra (abs_SNo t) r 1 HabRlt Hrlt1).
We prove the intermediate claim Hbddef: R_bounded_distance a b = If_i (Rlt (abs_SNo t) 1) (abs_SNo t) 1.
Use reflexivity.
rewrite the current goal using Hbddef (from left to right).
rewrite the current goal using (If_i_1 (Rlt (abs_SNo t) 1) (abs_SNo t) 1 Hablt1) (from left to right).
An exact proof term for the current goal is HabRlt.
∎