Let a and b be given.
Assume HaR: a ∈ R.
Assume HbR: b ∈ R.
Assume Hbd0: R_bounded_distance a b = 0.
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
We prove the intermediate claim HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
Set t to be the term add_SNo a (minus_SNo b).
We prove the intermediate claim HtR: t ∈ R.
We prove the intermediate claim HmbR: minus_SNo b ∈ R.
An exact proof term for the current goal is (real_minus_SNo b HbR).
An exact proof term for the current goal is (real_add_SNo a HaR (minus_SNo b) HmbR).
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 Hdef: R_bounded_distance a b = If_i (Rlt (abs_SNo t) 1) (abs_SNo t) 1.
Use reflexivity.
We prove the intermediate claim Hif0: If_i (Rlt (abs_SNo t) 1) (abs_SNo t) 1 = 0.
rewrite the current goal using Hdef (from right to left).
An exact proof term for the current goal is Hbd0.
Apply (xm (Rlt (abs_SNo t) 1) (a = b)) to the current goal.
Assume Hlt: Rlt (abs_SNo t) 1.
We prove the intermediate claim Ht0: t = 0.
We prove the intermediate claim Habs0: abs_SNo t = 0.
rewrite the current goal using (If_i_1 (Rlt (abs_SNo t) 1) (abs_SNo t) 1 Hlt) (from right to left).
An exact proof term for the current goal is Hif0.
An exact proof term for the current goal is (abs_SNo_eq0 t HtS Habs0).
We prove the intermediate claim Ht0': add_SNo a (minus_SNo b) = 0.
An exact proof term for the current goal is Ht0.
We prove the intermediate claim Hstep: add_SNo (add_SNo a (minus_SNo b)) b = b.
rewrite the current goal using Ht0' (from left to right) at position 1.
rewrite the current goal using (add_SNo_0L b HbS) (from left to right).
Use reflexivity.
rewrite the current goal using (add_SNo_0R a HaS) (from right to left) at position 1.
rewrite the current goal using (add_SNo_minus_SNo_linv b HbS) (from right to left) at position 1.
rewrite the current goal using (add_SNo_assoc a (minus_SNo b) b HaS (SNo_minus_SNo b HbS) HbS) (from left to right) at position 1.
An exact proof term for the current goal is Hstep.
Assume Hnlt: ¬ (Rlt (abs_SNo t) 1).
We prove the intermediate claim H10eq: 1 = 0.
rewrite the current goal using (If_i_0 (Rlt (abs_SNo t) 1) (abs_SNo t) 1 Hnlt) (from right to left).
An exact proof term for the current goal is Hif0.
We prove the intermediate claim H10: 1 ≠ 0.
An exact proof term for the current goal is neq_1_0.
An exact proof term for the current goal is (FalseE (H10 H10eq) (a = b)).
∎