Let a be given.

Assume HaR: a ∈ R.

We prove the intermediate claim HaS: SNo a.

An exact proof term for the current goal is (real_SNo a HaR).

Set t to be the term add_SNo a (minus_SNo a).

We prove the intermediate claim Ht0: t = 0.

An exact proof term for the current goal is (add_SNo_minus_SNo_rinv a HaS).

We prove the intermediate claim H0le0: 0 ≤ 0.

An exact proof term for the current goal is (SNoLe_ref 0).

We prove the intermediate claim Habseq: abs_SNo 0 = 0.

An exact proof term for the current goal is (nonneg_abs_SNo 0 H0le0).

We prove the intermediate claim Habs0: abs_SNo t = 0.

rewrite the current goal using Ht0 (from left to right).

An exact proof term for the current goal is Habseq.

We prove the intermediate claim Hdef: R_bounded_distance a a = If_i (Rlt (abs_SNo t) 1) (abs_SNo t) 1.

Use reflexivity.

rewrite the current goal using Hdef (from left to right).

rewrite the current goal using Habs0 (from left to right).

rewrite the current goal using (If_i_1 (Rlt 0 1) 0 1 Rlt_0_1) (from left to right).

Use reflexivity.

∎