Let seq and i be given.
Assume Hc: cauchy_sequence R_omega_space Romega_D_metric seq.
Assume HiO: i ∈ ω.
Set X to be the term R_omega_space.
Set d to be the term Romega_D_metric.
Set seqi to be the term product_coordinate_sequence seq i.
We prove the intermediate claim Hleft: metric_on X d ∧ sequence_on seq X.
An exact proof term for the current goal is (andEL (metric_on X d ∧ sequence_on seq X) (∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun d (apply_fun seq m,apply_fun seq n)) eps) Hc).
We prove the intermediate claim Hm: metric_on X d.
An exact proof term for the current goal is (andEL (metric_on X d) (sequence_on seq X) Hleft).
We prove the intermediate claim Hseq: sequence_on seq X.
An exact proof term for the current goal is (andER (metric_on X d) (sequence_on seq X) Hleft).
We prove the intermediate claim Htail: ∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun d (apply_fun seq m,apply_fun seq n)) eps.
An exact proof term for the current goal is (andER (metric_on X d ∧ sequence_on seq X) (∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun d (apply_fun seq m,apply_fun seq n)) eps) Hc).
We will prove metric_on R R_bounded_metric ∧ sequence_on seqi R ∧ ∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun R_bounded_metric (apply_fun seqi m,apply_fun seqi n)) eps.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is R_bounded_metric_is_metric_on.
Let n be given.
Assume HnO: n ∈ ω.
We will prove apply_fun seqi n ∈ R.
We prove the intermediate claim HseqnX: apply_fun seq n ∈ X.
An exact proof term for the current goal is (Hseq n HnO).
We prove the intermediate claim HseqiDef: seqi = graph ω (λk : set ⇒ apply_fun (apply_fun seq k) i).
Use reflexivity.
rewrite the current goal using HseqiDef (from left to right).
rewrite the current goal using (apply_fun_graph ω (λk : set ⇒ apply_fun (apply_fun seq k) i) n HnO) (from left to right).
An exact proof term for the current goal is (Romega_coord_in_R (apply_fun seq n) i HseqnX HiO).
Let eps be given.
Assume Heps: eps ∈ R ∧ Rlt 0 eps.
We prove the intermediate claim HepsR: eps ∈ R.
An exact proof term for the current goal is (andEL (eps ∈ R) (Rlt 0 eps) Heps).
We prove the intermediate claim HepsPos: Rlt 0 eps.
An exact proof term for the current goal is (andER (eps ∈ R) (Rlt 0 eps) Heps).
Set inv to be the term inv_nat (ordsucc i).
Set eps1 to be the term mul_SNo eps inv.
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 HinvS: SNo inv.
An exact proof term for the current goal is (real_SNo inv HinvR).
We prove the intermediate claim HinvNot0: ordsucc i ∉ {0}.
Assume Hin0: 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) Hin0).
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 HinvPos: Rlt 0 inv.
An exact proof term for the current goal is (inv_nat_pos (ordsucc i) HinvIn).
We prove the intermediate claim Heps1R: eps1 ∈ R.
An exact proof term for the current goal is (real_mul_SNo eps HepsR inv HinvR).
We prove the intermediate claim HepsS: SNo eps.
An exact proof term for the current goal is (real_SNo eps HepsR).
We prove the intermediate claim HepsPosS: 0 < eps.
An exact proof term for the current goal is (RltE_lt 0 eps HepsPos).
We prove the intermediate claim HinvPosS: 0 < inv.
An exact proof term for the current goal is (RltE_lt 0 inv HinvPos).
We prove the intermediate claim Heps1PosS: 0 < eps1.
An exact proof term for the current goal is (mul_SNo_pos_pos eps inv HepsS HinvS HepsPosS HinvPosS).
We prove the intermediate claim Heps1Pos: Rlt 0 eps1.
An exact proof term for the current goal is (RltI 0 eps1 real_0 Heps1R Heps1PosS).
We prove the intermediate claim Heps1pair: eps1 ∈ R ∧ Rlt 0 eps1.
Apply andI to the current goal.
An exact proof term for the current goal is Heps1R.
An exact proof term for the current goal is Heps1Pos.
We prove the intermediate claim HexN: ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun d (apply_fun seq m,apply_fun seq n)) eps1.
An exact proof term for the current goal is (Htail eps1 Heps1pair).
Apply HexN to the current goal.
Let N be given.
Assume HNpair.
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (N ∈ ω) (∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun d (apply_fun seq m,apply_fun seq n)) eps1) HNpair).
Let m and n be given.
Assume HmO: m ∈ ω.
Assume HnO: n ∈ ω.
Assume HNm: N ⊆ m.
Assume HNn: N ⊆ n.
We will prove Rlt (apply_fun R_bounded_metric (apply_fun seqi m,apply_fun seqi n)) eps.
We prove the intermediate claim HltD: Rlt (apply_fun d (apply_fun seq m,apply_fun seq n)) eps1.
An exact proof term for the current goal is (andER (N ∈ ω) (∀m0 n0 : set, m0 ∈ ω → n0 ∈ ω → N ⊆ m0 → N ⊆ n0 → Rlt (apply_fun d (apply_fun seq m0,apply_fun seq n0)) eps1) HNpair m n HmO HnO HNm HNn).
We prove the intermediate claim HseqmX: apply_fun seq m ∈ X.
An exact proof term for the current goal is (Hseq m HmO).
We prove the intermediate claim HseqnX: apply_fun seq n ∈ X.
An exact proof term for the current goal is (Hseq n HnO).
We prove the intermediate claim Hmnprod: (apply_fun seq m,apply_fun seq n) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X (apply_fun seq m) (apply_fun seq n) HseqmX HseqnX).
We prove the intermediate claim Hdapp: apply_fun d (apply_fun seq m,apply_fun seq n) = Romega_D_metric_value (apply_fun seq m) (apply_fun seq n).
rewrite the current goal using (apply_fun_graph (setprod X X) (λp : set ⇒ Romega_D_metric_value (p 0) (p 1)) (apply_fun seq m,apply_fun seq n) Hmnprod) (from left to right).
rewrite the current goal using (tuple_2_0_eq (apply_fun seq m) (apply_fun seq n)) (from left to right).
rewrite the current goal using (tuple_2_1_eq (apply_fun seq m) (apply_fun seq n)) (from left to right).
Use reflexivity.
We prove the intermediate claim HltVal: Rlt (Romega_D_metric_value (apply_fun seq m) (apply_fun seq n)) eps1.
rewrite the current goal using Hdapp (from right to left).
An exact proof term for the current goal is HltD.
We prove the intermediate claim Hscaled: Rlt (mul_SNo (R_bounded_distance (apply_fun (apply_fun seq m) i) (apply_fun (apply_fun seq n) i)) inv) eps1.
An exact proof term for the current goal is (Romega_D_metric_value_lt_implies_scaled_lt (apply_fun seq m) (apply_fun seq n) i eps1 HseqmX HseqnX HiO HltVal).
We prove the intermediate claim HscaledS: mul_SNo (R_bounded_distance (apply_fun (apply_fun seq m) i) (apply_fun (apply_fun seq n) i)) inv < eps1.
An exact proof term for the current goal is (RltE_lt (mul_SNo (R_bounded_distance (apply_fun (apply_fun seq m) i) (apply_fun (apply_fun seq n) i)) inv) eps1 Hscaled).
Set bd to be the term R_bounded_distance (apply_fun (apply_fun seq m) i) (apply_fun (apply_fun seq n) i).
We prove the intermediate claim HbdR: bd ∈ R.
An exact proof term for the current goal is (R_bounded_distance_in_R (apply_fun (apply_fun seq m) i) (apply_fun (apply_fun seq n) i) (Romega_coord_in_R (apply_fun seq m) i HseqmX HiO) (Romega_coord_in_R (apply_fun seq n) i HseqnX HiO)).
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 HepsInvEq: eps1 = mul_SNo eps inv.
Use reflexivity.
We prove the intermediate claim Hbdlt: bd < eps.
Apply (SNoLt_trichotomy_or_impred bd eps HbdS HepsS (bd < eps)) to the current goal.
Assume Hc0: bd < eps.
An exact proof term for the current goal is Hc0.
Assume Hc0: bd = eps.
We prove the intermediate claim Heqmul: mul_SNo bd inv = eps1.
rewrite the current goal using Hc0 (from left to right).
rewrite the current goal using HepsInvEq (from right to left).
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 HscaledS.
An exact proof term for the current goal is (FalseE ((SNoLt_irref (mul_SNo bd inv)) Hbad) (bd < eps)).
Assume Hc0: eps < bd.
We prove the intermediate claim Hmul: mul_SNo eps inv < mul_SNo bd inv.
An exact proof term for the current goal is (pos_mul_SNo_Lt' eps bd inv HepsS HbdS HinvS HinvPosS Hc0).
We prove the intermediate claim Hmul2: eps1 < mul_SNo bd inv.
rewrite the current goal using HepsInvEq (from left to right).
An exact proof term for the current goal is Hmul.
We prove the intermediate claim Hbad: mul_SNo eps inv < mul_SNo eps inv.
rewrite the current goal using HepsInvEq (from right to left) at position 1.
rewrite the current goal using HepsInvEq (from right to left) at position 2.
An exact proof term for the current goal is (SNoLt_tra eps1 (mul_SNo bd inv) eps1 (SNo_mul_SNo eps inv HepsS HinvS) (SNo_mul_SNo bd inv HbdS HinvS) (SNo_mul_SNo eps inv HepsS HinvS) Hmul2 HscaledS).
An exact proof term for the current goal is (FalseE ((SNoLt_irref eps1) Hbad) (bd < eps)).
We prove the intermediate claim HbdltR: Rlt bd eps.
An exact proof term for the current goal is (RltI bd eps HbdR HepsR Hbdlt).
We prove the intermediate claim HseqiDef: seqi = graph ω (λk : set ⇒ apply_fun (apply_fun seq k) i).
Use reflexivity.
rewrite the current goal using HseqiDef (from left to right).
rewrite the current goal using (apply_fun_graph ω (λk : set ⇒ apply_fun (apply_fun seq k) i) m HmO) (from left to right).
rewrite the current goal using (apply_fun_graph ω (λk : set ⇒ apply_fun (apply_fun seq k) i) n HnO) (from left to right).
rewrite the current goal using (R_bounded_metric_apply (apply_fun (apply_fun seq m) i) (apply_fun (apply_fun seq n) i) (Romega_coord_in_R (apply_fun seq m) i HseqmX HiO) (Romega_coord_in_R (apply_fun seq n) i HseqnX HiO)) (from left to right).
An exact proof term for the current goal is HbdltR.
∎