Let X, d, seq, x and y be given.
Assume Hd: metric_on X d.
Assume Hseq: sequence_on seq X.
Assume Hx: sequence_converges_metric X d seq x.
Assume Hy: sequence_converges_metric X d seq y.
We will prove x = y.
Apply xm (x = y) to the current goal.
An exact proof term for the current goal is (λH ⇒ H).
Assume Hneq: ¬ (x = y).
We will prove False.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (sequence_converges_metric_point_in_X X d seq x Hx).
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (sequence_converges_metric_point_in_X X d seq y Hy).
We prove the intermediate claim Hfun: function_on d (setprod X X) R.
An exact proof term for the current goal is (metric_on_function_on X d Hd).
We prove the intermediate claim HxyIn: (x,y) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x y HxX HyX).
We prove the intermediate claim HdxyR: apply_fun d (x,y) ∈ R.
An exact proof term for the current goal is (Hfun (x,y) HxyIn).
We prove the intermediate claim HdxyS: SNo (apply_fun d (x,y)).
An exact proof term for the current goal is (real_SNo (apply_fun d (x,y)) HdxyR).
We prove the intermediate claim HdxyNe0: ¬ (apply_fun d (x,y) = 0).
Assume H0: apply_fun d (x,y) = 0.
Apply Hneq to the current goal.
An exact proof term for the current goal is (metric_on_zero_eq X d x y Hd HxX HyX H0).
We prove the intermediate claim HdxyPos: Rlt 0 (apply_fun d (x,y)).
Apply (SNoLt_trichotomy_or_impred 0 (apply_fun d (x,y)) SNo_0 HdxyS (Rlt 0 (apply_fun d (x,y)))) to the current goal.
Assume H0lt: 0 < apply_fun d (x,y).
An exact proof term for the current goal is (RltI 0 (apply_fun d (x,y)) real_0 HdxyR H0lt).
Assume Heq: 0 = apply_fun d (x,y).
We will prove False.
We prove the intermediate claim H0eq: apply_fun d (x,y) = 0.
rewrite the current goal using Heq (from right to left).
Use reflexivity.
An exact proof term for the current goal is (HdxyNe0 H0eq).
Assume Hlt0: apply_fun d (x,y) < 0.
We will prove False.
We prove the intermediate claim HltR: Rlt (apply_fun d (x,y)) 0.
An exact proof term for the current goal is (RltI (apply_fun d (x,y)) 0 HdxyR real_0 Hlt0).
An exact proof term for the current goal is ((metric_on_nonneg X d x y Hd HxX HyX) HltR).
We prove the intermediate claim HexN: ∃N ∈ ω, eps_ N < apply_fun d (x,y).
An exact proof term for the current goal is (exists_eps_lt_pos (apply_fun d (x,y)) HdxyR HdxyPos).
Apply HexN to the current goal.
Let N be given.
Assume HNpair.
We prove the intermediate claim HNomega: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (eps_ N < apply_fun d (x,y)) HNpair).
We prove the intermediate claim HepsNlt: eps_ N < apply_fun d (x,y).
An exact proof term for the current goal is (andER (N ∈ ω) (eps_ N < apply_fun d (x,y)) HNpair).
We prove the intermediate claim HNnat: nat_p N.
An exact proof term for the current goal is (omega_nat_p N HNomega).
We prove the intermediate claim HsuccOmega: ordsucc N ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N HNomega).
We prove the intermediate claim HepsR: eps_ (ordsucc N) ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ (ordsucc N)) (SNo_eps_SNoS_omega (ordsucc N) HsuccOmega)).
We prove the intermediate claim HepsS: SNo (eps_ (ordsucc N)).
An exact proof term for the current goal is (SNo_eps_ (ordsucc N) HsuccOmega).
We prove the intermediate claim H0lt_eps: 0 < eps_ (ordsucc N).
An exact proof term for the current goal is (SNo_eps_pos (ordsucc N) HsuccOmega).
We prove the intermediate claim HepsPos: Rlt 0 (eps_ (ordsucc N)).
An exact proof term for the current goal is (RltI 0 (eps_ (ordsucc N)) real_0 HepsR H0lt_eps).
We prove the intermediate claim HexNx: ∃Nx : set, Nx ∈ ω ∧ ∀n : set, n ∈ ω → Nx ⊆ n → Rlt (apply_fun d (apply_fun seq n,x)) (eps_ (ordsucc N)).
An exact proof term for the current goal is (sequence_converges_metric_eps X d seq x Hx (eps_ (ordsucc N)) (andI (eps_ (ordsucc N) ∈ R) (Rlt 0 (eps_ (ordsucc N))) HepsR HepsPos)).
We prove the intermediate claim HexNy: ∃Ny : set, Ny ∈ ω ∧ ∀n : set, n ∈ ω → Ny ⊆ n → Rlt (apply_fun d (apply_fun seq n,y)) (eps_ (ordsucc N)).
An exact proof term for the current goal is (sequence_converges_metric_eps X d seq y Hy (eps_ (ordsucc N)) (andI (eps_ (ordsucc N) ∈ R) (Rlt 0 (eps_ (ordsucc N))) HepsR HepsPos)).
Apply HexNx to the current goal.
Let Nx be given.
Assume HNxpair.
Apply HexNy to the current goal.
Let Ny be given.
Assume HNypair.
We prove the intermediate claim HNxomega: Nx ∈ ω.
An exact proof term for the current goal is (andEL (Nx ∈ ω) (∀n : set, n ∈ ω → Nx ⊆ n → Rlt (apply_fun d (apply_fun seq n,x)) (eps_ (ordsucc N))) HNxpair).
We prove the intermediate claim HNxprop: ∀n : set, n ∈ ω → Nx ⊆ n → Rlt (apply_fun d (apply_fun seq n,x)) (eps_ (ordsucc N)).
An exact proof term for the current goal is (andER (Nx ∈ ω) (∀n : set, n ∈ ω → Nx ⊆ n → Rlt (apply_fun d (apply_fun seq n,x)) (eps_ (ordsucc N))) HNxpair).
We prove the intermediate claim HNyomega: Ny ∈ ω.
An exact proof term for the current goal is (andEL (Ny ∈ ω) (∀n : set, n ∈ ω → Ny ⊆ n → Rlt (apply_fun d (apply_fun seq n,y)) (eps_ (ordsucc N))) HNypair).
We prove the intermediate claim HNyprop: ∀n : set, n ∈ ω → Ny ⊆ n → Rlt (apply_fun d (apply_fun seq n,y)) (eps_ (ordsucc N)).
An exact proof term for the current goal is (andER (Ny ∈ ω) (∀n : set, n ∈ ω → Ny ⊆ n → Rlt (apply_fun d (apply_fun seq n,y)) (eps_ (ordsucc N))) HNypair).
Set n0 to be the term Nx ∪ Ny.
We prove the intermediate claim Hn0omega: n0 ∈ ω.
An exact proof term for the current goal is (omega_binunion Nx Ny HNxomega HNyomega).
We prove the intermediate claim HNxsub: Nx ⊆ n0.
An exact proof term for the current goal is (binunion_Subq_1 Nx Ny).
We prove the intermediate claim HNysub: Ny ⊆ n0.
An exact proof term for the current goal is (binunion_Subq_2 Nx Ny).
We prove the intermediate claim Hdx0: Rlt (apply_fun d (apply_fun seq n0,x)) (eps_ (ordsucc N)).
An exact proof term for the current goal is (HNxprop n0 Hn0omega HNxsub).
We prove the intermediate claim Hdy0: Rlt (apply_fun d (apply_fun seq n0,y)) (eps_ (ordsucc N)).
An exact proof term for the current goal is (HNyprop n0 Hn0omega HNysub).
We prove the intermediate claim Hseqfun: function_on seq ω X.
An exact proof term for the current goal is Hseq.
We prove the intermediate claim Hseqn0X: apply_fun seq n0 ∈ X.
An exact proof term for the current goal is (Hseqfun n0 Hn0omega).
We prove the intermediate claim HsymX: apply_fun d (x,apply_fun seq n0) = apply_fun d (apply_fun seq n0,x).
An exact proof term for the current goal is (metric_on_symmetric X d x (apply_fun seq n0) Hd HxX Hseqn0X).
We prove the intermediate claim Hdx: Rlt (apply_fun d (x,apply_fun seq n0)) (eps_ (ordsucc N)).
rewrite the current goal using HsymX (from left to right).
An exact proof term for the current goal is Hdx0.
Set a to be the term apply_fun d (x,apply_fun seq n0).
Set b to be the term apply_fun d (apply_fun seq n0,y).
We prove the intermediate claim Hxn0In: (x,apply_fun seq n0) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x (apply_fun seq n0) HxX Hseqn0X).
We prove the intermediate claim Hn0yIn: (apply_fun seq n0,y) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X (apply_fun seq n0) y Hseqn0X HyX).
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (Hfun (x,apply_fun seq n0) Hxn0In).
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is (Hfun (apply_fun seq n0,y) Hn0yIn).
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
We prove the intermediate claim HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim Haxlt: a < eps_ (ordsucc N).
An exact proof term for the current goal is (RltE_lt a (eps_ (ordsucc N)) Hdx).
We prove the intermediate claim Hbylt: b < eps_ (ordsucc N).
An exact proof term for the current goal is (RltE_lt b (eps_ (ordsucc N)) Hdy0).
We prove the intermediate claim Hstep1: add_SNo a b < add_SNo a (eps_ (ordsucc N)).
An exact proof term for the current goal is (add_SNo_Lt2 a b (eps_ (ordsucc N)) HaS HbS HepsS Hbylt).
We prove the intermediate claim Hstep2raw: add_SNo (eps_ (ordsucc N)) a < add_SNo (eps_ (ordsucc N)) (eps_ (ordsucc N)).
An exact proof term for the current goal is (add_SNo_Lt2 (eps_ (ordsucc N)) a (eps_ (ordsucc N)) HepsS HaS HepsS Haxlt).
We prove the intermediate claim Hcom: add_SNo (eps_ (ordsucc N)) a = add_SNo a (eps_ (ordsucc N)).
An exact proof term for the current goal is (add_SNo_com (eps_ (ordsucc N)) a HepsS HaS).
We prove the intermediate claim Hstep2: add_SNo a (eps_ (ordsucc N)) < add_SNo (eps_ (ordsucc N)) (eps_ (ordsucc N)).
rewrite the current goal using Hcom (from right to left) at position 1.
An exact proof term for the current goal is Hstep2raw.
We prove the intermediate claim Hsumlt_eps2: add_SNo a b < add_SNo (eps_ (ordsucc N)) (eps_ (ordsucc N)).
An exact proof term for the current goal is (SNoLt_tra (add_SNo a b) (add_SNo a (eps_ (ordsucc N))) (add_SNo (eps_ (ordsucc N)) (eps_ (ordsucc N))) (SNo_add_SNo a b HaS HbS) (SNo_add_SNo a (eps_ (ordsucc N)) HaS HepsS) (SNo_add_SNo (eps_ (ordsucc N)) (eps_ (ordsucc N)) HepsS HepsS) Hstep1 Hstep2).
We prove the intermediate claim HepsHalf: add_SNo (eps_ (ordsucc N)) (eps_ (ordsucc N)) = eps_ N.
An exact proof term for the current goal is (eps_ordsucc_half_add N HNnat).
We prove the intermediate claim HsumS: SNo (add_SNo a b).
An exact proof term for the current goal is (SNo_add_SNo a b HaS HbS).
We prove the intermediate claim HepsNR: eps_ N ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ N) (SNo_eps_SNoS_omega N HNomega)).
We prove the intermediate claim HepsNS: SNo (eps_ N).
An exact proof term for the current goal is (real_SNo (eps_ N) HepsNR).
We prove the intermediate claim Hsumlt_epsN: add_SNo a b < eps_ N.
rewrite the current goal using HepsHalf (from right to left).
An exact proof term for the current goal is Hsumlt_eps2.
We prove the intermediate claim Hsumlt_dxy: add_SNo a b < apply_fun d (x,y).
An exact proof term for the current goal is (SNoLt_tra (add_SNo a b) (eps_ N) (apply_fun d (x,y)) HsumS HepsNS HdxyS Hsumlt_epsN HepsNlt).
We prove the intermediate claim HsumR: add_SNo a b ∈ R.
An exact proof term for the current goal is (real_add_SNo a HaR b HbR).
We prove the intermediate claim HsumltR: Rlt (add_SNo a b) (apply_fun d (x,y)).
An exact proof term for the current goal is (RltI (add_SNo a b) (apply_fun d (x,y)) HsumR HdxyR Hsumlt_dxy).
We prove the intermediate claim Htri: ¬ (Rlt (add_SNo a b) (apply_fun d (x,y))).
An exact proof term for the current goal is (metric_on_triangle X d x (apply_fun seq n0) y Hd HxX Hseqn0X HyX).
An exact proof term for the current goal is (Htri HsumltR).
∎