Let a and b be given.
Assume HaR: a ∈ R.
Assume HbR: 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 Hor: If_i (Rlt (abs_SNo t) 1) (abs_SNo t) 1 = abs_SNo t ∨ If_i (Rlt (abs_SNo t) 1) (abs_SNo t) 1 = 1.
An exact proof term for the current goal is (If_i_or (Rlt (abs_SNo t) 1) (abs_SNo t) 1).
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 Hor to the current goal.
Assume Heq: If_i (Rlt (abs_SNo t) 1) (abs_SNo t) 1 = abs_SNo t.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HabsR.
Assume Heq: If_i (Rlt (abs_SNo t) 1) (abs_SNo t) 1 = 1.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is real_1.
∎