Let seq be given.

Assume Hseq: sequence_on seq R.

Assume Hc: cauchy_sequence R R_bounded_metric seq.

We prove the intermediate claim HabsTail: ∀eps0 : set, eps0 ∈ R → Rlt 0 eps0 → Rlt eps0 1 → ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → abs_SNo (add_SNo (apply_fun seq m) (minus_SNo (apply_fun seq n))) < eps0.

Let eps0 be given.

Assume Heps0R: eps0 ∈ R.

Assume Heps0Pos: Rlt 0 eps0.

Assume Heps0Lt1: Rlt eps0 1.

An exact proof term for the current goal is (cauchy_R_bounded_metric_abs_tail_early seq eps0 Hc Heps0R Heps0Pos Heps0Lt1).

We prove the intermediate claim HabC: ∀eps0 : set, eps0 ∈ R ∧ Rlt 0 eps0 → ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → abs_SNo (add_SNo (apply_fun seq m) (minus_SNo (apply_fun seq n))) < eps0.

Let eps0 be given.

Assume Heps0: eps0 ∈ R ∧ Rlt 0 eps0.

We prove the intermediate claim Heps0R: eps0 ∈ R.

An exact proof term for the current goal is (andEL (eps0 ∈ R) (Rlt 0 eps0) Heps0).

We prove the intermediate claim Heps0Pos: Rlt 0 eps0.

An exact proof term for the current goal is (andER (eps0 ∈ R) (Rlt 0 eps0) Heps0).

We prove the intermediate claim Hexd: ∃d : set, d ∈ R ∧ Rlt 0 d ∧ Rlt d eps0 ∧ Rlt d 1 ∧ Rlt d 1 ∧ Rlt d 1.

An exact proof term for the current goal is (exists_eps_lt_four_pos_Euclid eps0 1 1 1 Heps0R real_1 real_1 real_1 Heps0Pos Rlt_0_1 Rlt_0_1 Rlt_0_1).

Apply Hexd to the current goal.

Let d be given.

Assume Hd: d ∈ R ∧ Rlt 0 d ∧ Rlt d eps0 ∧ Rlt d 1 ∧ Rlt d 1 ∧ Rlt d 1.

We prove the intermediate claim HdABCDE: ((((d ∈ R ∧ Rlt 0 d) ∧ Rlt d eps0) ∧ Rlt d 1) ∧ Rlt d 1).

An exact proof term for the current goal is (andEL ((((d ∈ R ∧ Rlt 0 d) ∧ Rlt d eps0) ∧ Rlt d 1) ∧ Rlt d 1) (Rlt d 1) Hd).

We prove the intermediate claim HdABCD: (((d ∈ R ∧ Rlt 0 d) ∧ Rlt d eps0) ∧ Rlt d 1).

An exact proof term for the current goal is (andEL (((d ∈ R ∧ Rlt 0 d) ∧ Rlt d eps0) ∧ Rlt d 1) (Rlt d 1) HdABCDE).

We prove the intermediate claim HdABC: ((d ∈ R ∧ Rlt 0 d) ∧ Rlt d eps0).

An exact proof term for the current goal is (andEL ((d ∈ R ∧ Rlt 0 d) ∧ Rlt d eps0) (Rlt d 1) HdABCD).

We prove the intermediate claim HdD: Rlt d 1.

An exact proof term for the current goal is (andER ((d ∈ R ∧ Rlt 0 d) ∧ Rlt d eps0) (Rlt d 1) HdABCD).

We prove the intermediate claim HdAB: d ∈ R ∧ Rlt 0 d.

An exact proof term for the current goal is (andEL (d ∈ R ∧ Rlt 0 d) (Rlt d eps0) HdABC).

We prove the intermediate claim Hdeps0: Rlt d eps0.

An exact proof term for the current goal is (andER (d ∈ R ∧ Rlt 0 d) (Rlt d eps0) HdABC).

We prove the intermediate claim HdR: d ∈ R.

An exact proof term for the current goal is (andEL (d ∈ R) (Rlt 0 d) HdAB).

We prove the intermediate claim HdPos: Rlt 0 d.

An exact proof term for the current goal is (andER (d ∈ R) (Rlt 0 d) HdAB).

We prove the intermediate claim Hdlt1: Rlt d 1.

An exact proof term for the current goal is HdD.

We prove the intermediate claim HexN: ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → abs_SNo (add_SNo (apply_fun seq m) (minus_SNo (apply_fun seq n))) < d.

An exact proof term for the current goal is (HabsTail d HdR HdPos Hdlt1).

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 → abs_SNo (add_SNo (apply_fun seq m) (minus_SNo (apply_fun seq n))) < d) HNpair).

Let m and n be given.

Assume HmO: m ∈ ω.

Assume HnO: n ∈ ω.

Assume HNm: N ⊆ m.

Assume HNn: N ⊆ n.

We will prove abs_SNo (add_SNo (apply_fun seq m) (minus_SNo (apply_fun seq n))) < eps0.

We prove the intermediate claim Habd: abs_SNo (add_SNo (apply_fun seq m) (minus_SNo (apply_fun seq n))) < d.

An exact proof term for the current goal is (andER (N ∈ ω) (∀m0 n0 : set, m0 ∈ ω → n0 ∈ ω → N ⊆ m0 → N ⊆ n0 → abs_SNo (add_SNo (apply_fun seq m0) (minus_SNo (apply_fun seq n0))) < d) HNpair m n HmO HnO HNm HNn).

We prove the intermediate claim HdS: SNo d.

An exact proof term for the current goal is (real_SNo d HdR).

We prove the intermediate claim Heps0S: SNo eps0.

An exact proof term for the current goal is (real_SNo eps0 Heps0R).

We prove the intermediate claim Hdeps0S: d < eps0.

An exact proof term for the current goal is (RltE_lt d eps0 Hdeps0).

We prove the intermediate claim HmR: apply_fun seq m ∈ R.

An exact proof term for the current goal is (Hseq m HmO).

We prove the intermediate claim HnR: apply_fun seq n ∈ R.

An exact proof term for the current goal is (Hseq n HnO).

We prove the intermediate claim HmnR: add_SNo (apply_fun seq m) (minus_SNo (apply_fun seq n)) ∈ R.

An exact proof term for the current goal is (real_add_SNo (apply_fun seq m) HmR (minus_SNo (apply_fun seq n)) (real_minus_SNo (apply_fun seq n) HnR)).

We prove the intermediate claim HabsR: abs_SNo (add_SNo (apply_fun seq m) (minus_SNo (apply_fun seq n))) ∈ R.

An exact proof term for the current goal is (abs_SNo_in_R (add_SNo (apply_fun seq m) (minus_SNo (apply_fun seq n))) HmnR).

We prove the intermediate claim HabsS: SNo (abs_SNo (add_SNo (apply_fun seq m) (minus_SNo (apply_fun seq n)))).

An exact proof term for the current goal is (real_SNo (abs_SNo (add_SNo (apply_fun seq m) (minus_SNo (apply_fun seq n)))) HabsR).

An exact proof term for the current goal is (SNoLt_tra (abs_SNo (add_SNo (apply_fun seq m) (minus_SNo (apply_fun seq n)))) d eps0 HabsS HdS Heps0S Habd Hdeps0S).

We prove the intermediate claim HexStd: ∃x : set, converges_to R R_standard_topology seq x.

An exact proof term for the current goal is (abs_Cauchy_sequence_converges_R_standard_topology_early seq Hseq HabC).

Apply HexStd to the current goal.

Let x be given.

Assume HxStd: converges_to R R_standard_topology seq x.

We use x to witness the existential quantifier.

We will prove converges_to R (metric_topology R R_bounded_metric) seq x.

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

An exact proof term for the current goal is HxStd.