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.
Apply (xm (0 ≤ t)) to the current goal.
Assume H0le: 0 ≤ t.
We prove the intermediate claim Habseq: abs_SNo t = t.
An exact proof term for the current goal is (nonneg_abs_SNo t H0le).
rewrite the current goal using Habseq (from left to right).
An exact proof term for the current goal is HtR.
Assume Hn0le: ¬ (0 ≤ t).
We prove the intermediate claim HmtR: minus_SNo t ∈ R.
An exact proof term for the current goal is (real_minus_SNo t HtR).
We prove the intermediate claim Habseq: abs_SNo t = minus_SNo t.
An exact proof term for the current goal is (not_nonneg_abs_SNo t Hn0le).
rewrite the current goal using Habseq (from left to right).
An exact proof term for the current goal is HmtR.
We prove the intermediate claim HdistR: R_bounded_distance a b ∈ R.
We prove the intermediate claim Hdef: R_bounded_distance a b = If_i (Rlt (abs_SNo t) 1) (abs_SNo t) 1.
Use reflexivity.
Apply (xm (Rlt (abs_SNo t) 1)) to the current goal.
Assume Hlt: Rlt (abs_SNo t) 1.
rewrite the current goal using Hdef (from left to right).
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 HabsR.
Assume Hnlt: ¬ (Rlt (abs_SNo t) 1).
rewrite the current goal using Hdef (from left to right).
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 real_1.
Apply (RleI (R_bounded_distance a b) 1 HdistR real_1) to the current goal.
We will prove ¬ (Rlt 1 (R_bounded_distance a b)).
We prove the intermediate claim Hdef: R_bounded_distance a b = If_i (Rlt (abs_SNo t) 1) (abs_SNo t) 1.
Use reflexivity.
Apply (xm (Rlt (abs_SNo t) 1)) to the current goal.
Assume Hlt: Rlt (abs_SNo t) 1.
rewrite the current goal using Hdef (from left to right).
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 (not_Rlt_sym (abs_SNo t) 1 Hlt).
Assume Hnlt: ¬ (Rlt (abs_SNo t) 1).
rewrite the current goal using Hdef (from left to right).
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 (not_Rlt_refl 1 real_1).
∎