Let x, y, i and delta be given.
Assume Hx: x ∈ R_omega_space.
Assume Hy: y ∈ R_omega_space.
Assume HiO: i ∈ ω.
Assume HdR: delta ∈ R.
Assume Hdpos: Rlt 0 delta.
Assume Hdlt1: Rlt delta 1.
Assume Hlt: Rlt (Romega_D_metric_value x y) (mul_SNo delta (inv_nat (ordsucc i))).
Set xi to be the term apply_fun x i.
Set yi to be the term apply_fun y i.
Set bd to be the term R_bounded_distance xi yi.
Set inv to be the term inv_nat (ordsucc i).
We prove the intermediate claim HxiR: xi ∈ R.
An exact proof term for the current goal is (Romega_coord_in_R x i Hx HiO).
We prove the intermediate claim HyiR: yi ∈ R.
An exact proof term for the current goal is (Romega_coord_in_R y i Hy HiO).
We prove the intermediate claim HbdR: bd ∈ R.
An exact proof term for the current goal is (R_bounded_distance_in_R xi yi HxiR HyiR).
We prove the intermediate claim HsuccO: ordsucc i ∈ ω.
An exact proof term for the current goal is (omega_ordsucc i HiO).
We prove the intermediate claim HinvR: inv ∈ R.
An exact proof term for the current goal is (inv_nat_real (ordsucc i) HsuccO).
We prove the intermediate claim HinvNot0: ordsucc i ∉ {0}.
Assume Hi0: ordsucc i ∈ {0}.
We prove the intermediate claim Heq0: ordsucc i = 0.
An exact proof term for the current goal is (SingE 0 (ordsucc i) Hi0).
An exact proof term for the current goal is (neq_ordsucc_0 i Heq0).
We prove the intermediate claim HinvIn: ordsucc i ∈ ω ∖ {0}.
An exact proof term for the current goal is (setminusI ω {0} (ordsucc i) HsuccO HinvNot0).
We prove the intermediate claim HinvPosR: Rlt 0 inv.
An exact proof term for the current goal is (inv_nat_pos (ordsucc i) HinvIn).
We prove the intermediate claim HinvPos: 0 < inv.
An exact proof term for the current goal is (RltE_lt 0 inv HinvPosR).
We prove the intermediate claim HbdS: SNo bd.
An exact proof term for the current goal is (real_SNo bd HbdR).
We prove the intermediate claim HdS: SNo delta.
An exact proof term for the current goal is (real_SNo delta HdR).
We prove the intermediate claim HinvS: SNo inv.
An exact proof term for the current goal is (real_SNo inv HinvR).
We prove the intermediate claim Hscaledlt: Rlt (mul_SNo bd inv) (mul_SNo delta inv).
An exact proof term for the current goal is (Romega_D_metric_value_lt_implies_scaled_lt x y i (mul_SNo delta inv) Hx Hy HiO Hlt).
We prove the intermediate claim HscaledltS: mul_SNo bd inv < mul_SNo delta inv.
An exact proof term for the current goal is (RltE_lt (mul_SNo bd inv) (mul_SNo delta inv) Hscaledlt).
We prove the intermediate claim Hbdlt: bd < delta.
Apply (SNoLt_trichotomy_or_impred bd delta HbdS HdS (bd < delta)) to the current goal.
Assume Hc: bd < delta.
An exact proof term for the current goal is Hc.
Assume Hc: bd = delta.
We prove the intermediate claim Heqmul: mul_SNo bd inv = mul_SNo delta inv.
rewrite the current goal using Hc (from left to right).
Use reflexivity.
We prove the intermediate claim Hbad: mul_SNo bd inv < mul_SNo bd inv.
rewrite the current goal using Heqmul (from left to right) at position 2.
An exact proof term for the current goal is HscaledltS.
An exact proof term for the current goal is (FalseE ((SNoLt_irref (mul_SNo bd inv)) Hbad) (bd < delta)).
Assume Hc: delta < bd.
We prove the intermediate claim Hmul: mul_SNo delta inv < mul_SNo bd inv.
An exact proof term for the current goal is (pos_mul_SNo_Lt' delta bd inv HdS HbdS HinvS HinvPos Hc).
We prove the intermediate claim Hbad: mul_SNo delta inv < mul_SNo delta inv.
An exact proof term for the current goal is (SNoLt_tra (mul_SNo delta inv) (mul_SNo bd inv) (mul_SNo delta inv) (SNo_mul_SNo delta inv HdS HinvS) (SNo_mul_SNo bd inv HbdS HinvS) (SNo_mul_SNo delta inv HdS HinvS) Hmul HscaledltS).
An exact proof term for the current goal is (FalseE ((SNoLt_irref (mul_SNo delta inv)) Hbad) (bd < delta)).
We prove the intermediate claim HbdRlt: Rlt bd delta.
An exact proof term for the current goal is (RltI bd delta HbdR HdR Hbdlt).
Set t to be the term add_SNo xi (minus_SNo yi).
An exact proof term for the current goal is (R_bounded_distance_lt_lt1_imp_abs_lt xi yi delta HxiR HyiR HdR Hdlt1 HbdRlt).
∎