Let seq and eps be given.
Assume Hc: cauchy_sequence R R_bounded_metric seq.
Assume HepsR: eps ∈ R.
Assume HepsPos: Rlt 0 eps.
Assume HepsLt1: Rlt eps 1.
We prove the intermediate claim Hleft: metric_on R R_bounded_metric ∧ sequence_on seq R.
An exact proof term for the current goal is (andEL (metric_on R R_bounded_metric ∧ sequence_on seq R) (∀eps0 : set, eps0 ∈ R ∧ Rlt 0 eps0 → ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun R_bounded_metric (apply_fun seq m,apply_fun seq n)) eps0) Hc).
We prove the intermediate claim Hseq: sequence_on seq R.
An exact proof term for the current goal is (andER (metric_on R R_bounded_metric) (sequence_on seq R) Hleft).
We prove the intermediate claim Htail: ∀eps0 : set, eps0 ∈ R ∧ Rlt 0 eps0 → ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun R_bounded_metric (apply_fun seq m,apply_fun seq n)) eps0.
An exact proof term for the current goal is (andER (metric_on R R_bounded_metric ∧ sequence_on seq R) (∀eps0 : set, eps0 ∈ R ∧ Rlt 0 eps0 → ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun R_bounded_metric (apply_fun seq m,apply_fun seq n)) eps0) Hc).
We prove the intermediate claim HepsPair: eps ∈ R ∧ Rlt 0 eps.
Apply andI to the current goal.
An exact proof term for the current goal is HepsR.
An exact proof term for the current goal is HepsPos.
Apply (Htail eps HepsPair) 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 R_bounded_metric (apply_fun seq m,apply_fun seq n)) eps) 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))) < eps.
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 Hlt: Rlt (apply_fun R_bounded_metric (apply_fun seq m,apply_fun seq n)) eps.
An exact proof term for the current goal is (andER (N ∈ ω) (∀m0 n0 : set, m0 ∈ ω → n0 ∈ ω → N ⊆ m0 → N ⊆ n0 → Rlt (apply_fun R_bounded_metric (apply_fun seq m0,apply_fun seq n0)) eps) HNpair m n HmO HnO HNm HNn).
We prove the intermediate claim Hlt2: Rlt (R_bounded_distance (apply_fun seq m) (apply_fun seq n)) eps.
rewrite the current goal using (R_bounded_metric_apply_early (apply_fun seq m) (apply_fun seq n) HmR HnR) (from right to left).
An exact proof term for the current goal is Hlt.
An exact proof term for the current goal is (R_bounded_distance_lt_lt1_imp_abs_lt (apply_fun seq m) (apply_fun seq n) eps HmR HnR HepsR HepsLt1 Hlt2).
∎