Let x and y be given.
Assume Hx: x ∈ R_omega_space.
Assume Hy: y ∈ R_omega_space.
We use 1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is real_1.
Let a be given.
Assume HaA: a ∈ Romega_D_scaled_diffs x y.
Assume HaR: a ∈ R.
We will prove Rle a 1.
Apply (ReplE_impred ω (λi : set ⇒ mul_SNo (R_bounded_distance (apply_fun x i) (apply_fun y i)) (inv_nat (ordsucc i))) a HaA (Rle a 1)) to the current goal.
Let i be given.
Assume HiO: i ∈ ω.
Assume Hai: a = mul_SNo (R_bounded_distance (apply_fun x i) (apply_fun y i)) (inv_nat (ordsucc i)).
rewrite the current goal using Hai (from left to right).
Set bd to be the term R_bounded_distance (apply_fun x i) (apply_fun y i).
Set inv to be the term inv_nat (ordsucc i).
We prove the intermediate claim HSi: ordsucc i ∈ ω.
An exact proof term for the current goal is (omega_ordsucc i HiO).
We prove the intermediate claim HsuccNotIn0: ordsucc i ∉ {0}.
Assume Hin0: ordsucc i ∈ {0}.
We prove the intermediate claim Heq: ordsucc i = 0.
An exact proof term for the current goal is (SingE 0 (ordsucc i) Hin0).
An exact proof term for the current goal is (neq_ordsucc_0 i Heq).
We prove the intermediate claim HiIn: ordsucc i ∈ ω ∖ {0}.
An exact proof term for the current goal is (setminusI ω {0} (ordsucc i) HSi HsuccNotIn0).
We prove the intermediate claim HxiR: apply_fun x i ∈ R.
An exact proof term for the current goal is (Romega_coord_in_R x i Hx HiO).
We prove the intermediate claim HyiR: apply_fun y i ∈ 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 (apply_fun x i) (apply_fun y i) HxiR HyiR).
We prove the intermediate claim HinvR: inv ∈ R.
An exact proof term for the current goal is (inv_nat_real (ordsucc i) HSi).
We prove the intermediate claim HmulR: mul_SNo bd inv ∈ R.
An exact proof term for the current goal is (real_mul_SNo bd HbdR inv HinvR).
Apply (RleI (mul_SNo bd inv) 1 HmulR real_1) to the current goal.
Assume Hlt1: Rlt 1 (mul_SNo bd inv).
We will prove False.
We prove the intermediate claim H1lt: 1 < mul_SNo bd inv.
An exact proof term for the current goal is (RltE_lt 1 (mul_SNo bd inv) Hlt1).
We prove the intermediate claim HbdRle1: Rle bd 1.
An exact proof term for the current goal is (R_bounded_distance_le_1 (apply_fun x i) (apply_fun y i) HxiR HyiR).
We prove the intermediate claim HinvRle1: Rle inv 1.
An exact proof term for the current goal is (inv_nat_Rle_1 (ordsucc i) HiIn).
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 HinvS: SNo inv.
An exact proof term for the current goal is (real_SNo inv HinvR).
We prove the intermediate claim HmulS: SNo (mul_SNo bd inv).
An exact proof term for the current goal is (real_SNo (mul_SNo bd inv) HmulR).
We prove the intermediate claim H0ltInvR: Rlt 0 inv.
An exact proof term for the current goal is (inv_nat_pos (ordsucc i) HiIn).
We prove the intermediate claim H0ltInv: 0 < inv.
An exact proof term for the current goal is (RltE_lt 0 inv H0ltInvR).
We prove the intermediate claim H0leInv: 0 ≤ inv.
An exact proof term for the current goal is (SNoLtLe 0 inv H0ltInv).
We prove the intermediate claim HbdLe1: bd ≤ 1.
Apply (SNoLt_trichotomy_or_impred bd 1 HbdS SNo_1 (bd ≤ 1)) to the current goal.
Assume Hlt: bd < 1.
An exact proof term for the current goal is (SNoLtLe bd 1 Hlt).
Assume Heq: bd = 1.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (SNoLe_ref 1).
Assume H1ltbd: 1 < bd.
Apply FalseE to the current goal.
We prove the intermediate claim HbdRlt: Rlt 1 bd.
An exact proof term for the current goal is (RltI 1 bd real_1 HbdR H1ltbd).
An exact proof term for the current goal is ((RleE_nlt bd 1 HbdRle1) HbdRlt).
We prove the intermediate claim HinvLe1: inv ≤ 1.
Apply (SNoLt_trichotomy_or_impred inv 1 HinvS SNo_1 (inv ≤ 1)) to the current goal.
Assume Hlt: inv < 1.
An exact proof term for the current goal is (SNoLtLe inv 1 Hlt).
Assume Heq: inv = 1.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (SNoLe_ref 1).
Assume H1ltinv: 1 < inv.
Apply FalseE to the current goal.
We prove the intermediate claim HinvRlt: Rlt 1 inv.
An exact proof term for the current goal is (RltI 1 inv real_1 HinvR H1ltinv).
An exact proof term for the current goal is ((RleE_nlt inv 1 HinvRle1) HinvRlt).
We prove the intermediate claim HmulLeInv: mul_SNo bd inv ≤ inv.
An exact proof term for the current goal is (mul_SNo_Le1_nonneg_Le bd inv HbdS HinvS HbdLe1 H0leInv).
We prove the intermediate claim HmulLe1: mul_SNo bd inv ≤ 1.
An exact proof term for the current goal is (SNoLe_tra (mul_SNo bd inv) inv 1 HmulS HinvS SNo_1 HmulLeInv HinvLe1).
We prove the intermediate claim Hcase: mul_SNo bd inv < 1 ∨ mul_SNo bd inv = 1.
An exact proof term for the current goal is (SNoLeE (mul_SNo bd inv) 1 HmulS SNo_1 HmulLe1).
Apply (Hcase False) to the current goal.
Assume HmulLt1: mul_SNo bd inv < 1.
We prove the intermediate claim H11: 1 < 1.
An exact proof term for the current goal is (SNoLt_tra 1 (mul_SNo bd inv) 1 SNo_1 HmulS SNo_1 H1lt HmulLt1).
An exact proof term for the current goal is ((SNoLt_irref 1) H11).
Assume HmulEq1: mul_SNo bd inv = 1.
We prove the intermediate claim H11: 1 < 1.
rewrite the current goal using HmulEq1 (from right to left) at position 2.
An exact proof term for the current goal is H1lt.
An exact proof term for the current goal is ((SNoLt_irref 1) H11).
∎