Let X, d, x, y and A be given.
Assume Hm: metric_on X d.
Assume HxX: x ∈ X.
Assume HyX: y ∈ X.
Assume HAsub: A ⊆ X.
Assume HAne: A ≠ Empty.
Set distx to be the term metric_dist_to_set X d x A.
Set disty to be the term metric_dist_to_set X d y A.
We prove the intermediate claim HdistxR: distx ∈ R.
An exact proof term for the current goal is (metric_dist_to_set_in_R X d x A Hm HxX HAsub HAne).
We prove the intermediate claim HdistyR: disty ∈ R.
An exact proof term for the current goal is (metric_dist_to_set_in_R X d y A Hm HyX HAsub HAne).
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 Hm).
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).
Set q to be the term add_SNo distx (apply_fun d (x,y)).
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (real_add_SNo distx HdistxR (apply_fun d (x,y)) HdxyR).
Apply (RleI disty q HdistyR HqR) to the current goal.
Assume Hlt: Rlt q disty.
Set diff to be the term add_SNo disty (minus_SNo q).
We prove the intermediate claim HdiffR: diff ∈ R.
An exact proof term for the current goal is (real_add_SNo disty HdistyR (minus_SNo q) (real_minus_SNo q HqR)).
We prove the intermediate claim HdiffPos: Rlt 0 diff.
An exact proof term for the current goal is (Rlt_0_diff_of_lt q disty Hlt).
We prove the intermediate claim HexN0: ∃N0 ∈ ω, eps_ N0 < diff.
An exact proof term for the current goal is (exists_eps_lt_pos diff HdiffR HdiffPos).
Apply HexN0 to the current goal.
Let N0 be given.
Assume HN0pair.
We prove the intermediate claim HN0omega: N0 ∈ ω.
An exact proof term for the current goal is (andEL (N0 ∈ ω) (eps_ N0 < diff) HN0pair).
We prove the intermediate claim Hepslt: eps_ N0 < diff.
An exact proof term for the current goal is (andER (N0 ∈ ω) (eps_ N0 < diff) HN0pair).
Set eps0 to be the term eps_ N0.
We prove the intermediate claim Heps0R: eps0 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real eps0 (SNo_eps_SNoS_omega N0 HN0omega)).
We prove the intermediate claim Heps0posS: 0 < eps0.
An exact proof term for the current goal is (SNo_eps_pos N0 HN0omega).
We prove the intermediate claim Heps0pos: Rlt 0 eps0.
An exact proof term for the current goal is (RltI 0 eps0 real_0 Heps0R Heps0posS).
We prove the intermediate claim Heps0ltDiffR: Rlt eps0 diff.
An exact proof term for the current goal is (RltI eps0 diff Heps0R HdiffR Hepslt).
We prove the intermediate claim Heps0ltDiffS: eps0 < diff.
An exact proof term for the current goal is (RltE_lt eps0 diff Heps0ltDiffR).
We prove the intermediate claim HqS: SNo q.
An exact proof term for the current goal is (real_SNo q HqR).
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 HdiffS: SNo diff.
An exact proof term for the current goal is (real_SNo diff HdiffR).
We prove the intermediate claim HqepsLt: add_SNo q eps0 < add_SNo q diff.
An exact proof term for the current goal is (add_SNo_Lt2 q eps0 diff HqS Heps0S HdiffS Heps0ltDiffS).
We prove the intermediate claim HqdiffEq: add_SNo q diff = disty.
We prove the intermediate claim HdistyS: SNo disty.
An exact proof term for the current goal is (real_SNo disty HdistyR).
We prove the intermediate claim HqSNo: SNo distx.
An exact proof term for the current goal is (real_SNo distx HdistxR).
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 HmqR: minus_SNo q ∈ R.
An exact proof term for the current goal is (real_minus_SNo q HqR).
We prove the intermediate claim HmqS: SNo (minus_SNo q).
An exact proof term for the current goal is (real_SNo (minus_SNo q) HmqR).
We prove the intermediate claim HdiffDef: diff = add_SNo disty (minus_SNo q).
Use reflexivity.
rewrite the current goal using HdiffDef (from left to right).
rewrite the current goal using (add_SNo_assoc q disty (minus_SNo q) HqS HdistyS HmqS) (from left to right).
rewrite the current goal using (add_SNo_com q disty HqS HdistyS) (from left to right).
rewrite the current goal using (add_SNo_assoc disty q (minus_SNo q) HdistyS HqS HmqS) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_rinv q HqS) (from left to right).
rewrite the current goal using (add_SNo_0R disty HdistyS) (from left to right).
Use reflexivity.
We prove the intermediate claim HqepsRlt: Rlt (add_SNo q eps0) disty.
rewrite the current goal using HqdiffEq (from right to left).
An exact proof term for the current goal is (RltI (add_SNo q eps0) (add_SNo q diff) (real_add_SNo q HqR eps0 Heps0R) (real_add_SNo q HqR diff HdiffR) HqepsLt).
We prove the intermediate claim Hexa: ∃a : set, a ∈ A ∧ a ∈ X ∧ Rlt (apply_fun d (x,a)) (add_SNo distx eps0).
An exact proof term for the current goal is (metric_dist_to_set_approx X d x A eps0 Hm HxX HAsub HAne Heps0R Heps0pos).
Apply Hexa to the current goal.
Let a be given.
Assume Hapack.
We prove the intermediate claim HaCore: a ∈ A ∧ a ∈ X.
An exact proof term for the current goal is (andEL (a ∈ A ∧ a ∈ X) (Rlt (apply_fun d (x,a)) (add_SNo distx eps0)) Hapack).
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (andEL (a ∈ A) (a ∈ X) HaCore).
We prove the intermediate claim HaX: a ∈ X.
An exact proof term for the current goal is (andER (a ∈ A) (a ∈ X) HaCore).
We prove the intermediate claim HdxaIn: (x,a) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x a HxX HaX).
We prove the intermediate claim HdyaIn: (y,a) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X y a HyX HaX).
We prove the intermediate claim HdxaR: apply_fun d (x,a) ∈ R.
An exact proof term for the current goal is (Hfun (x,a) HdxaIn).
We prove the intermediate claim HdyaR: apply_fun d (y,a) ∈ R.
An exact proof term for the current goal is (Hfun (y,a) HdyaIn).
We prove the intermediate claim Hdxalt: Rlt (apply_fun d (x,a)) (add_SNo distx eps0).
An exact proof term for the current goal is (andER (a ∈ A ∧ a ∈ X) (Rlt (apply_fun d (x,a)) (add_SNo distx eps0)) Hapack).
We prove the intermediate claim HdxySym: apply_fun d (y,x) = apply_fun d (x,y).
An exact proof term for the current goal is (metric_on_symmetric X d y x Hm HyX HxX).
We prove the intermediate claim HdxyR2: apply_fun d (y,x) ∈ R.
An exact proof term for the current goal is (Hfun (y,x) (tuple_2_setprod_by_pair_Sigma X X y x HyX HxX)).
We prove the intermediate claim HsumR1: add_SNo (apply_fun d (y,x)) (apply_fun d (x,a)) ∈ R.
An exact proof term for the current goal is (real_add_SNo (apply_fun d (y,x)) HdxyR2 (apply_fun d (x,a)) HdxaR).
We prove the intermediate claim HsumR2: add_SNo (apply_fun d (x,y)) (apply_fun d (x,a)) ∈ R.
An exact proof term for the current goal is (real_add_SNo (apply_fun d (x,y)) HdxyR (apply_fun d (x,a)) HdxaR).
We prove the intermediate claim HtriLe: Rle (apply_fun d (y,a)) (add_SNo (apply_fun d (y,x)) (apply_fun d (x,a))).
Apply (RleI (apply_fun d (y,a)) (add_SNo (apply_fun d (y,x)) (apply_fun d (x,a))) HdyaR HsumR1) to the current goal.
Assume Hbad: Rlt (add_SNo (apply_fun d (y,x)) (apply_fun d (x,a))) (apply_fun d (y,a)).
An exact proof term for the current goal is ((metric_on_triangle X d y x a Hm HyX HxX HaX) Hbad).
We prove the intermediate claim HtriLe2: Rle (apply_fun d (y,a)) (add_SNo (apply_fun d (x,y)) (apply_fun d (x,a))).
rewrite the current goal using HdxySym (from right to left).
An exact proof term for the current goal is HtriLe.
We prove the intermediate claim Hdyalt: Rlt (apply_fun d (y,a)) (add_SNo q eps0).
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 HdxaS: SNo (apply_fun d (x,a)).
An exact proof term for the current goal is (real_SNo (apply_fun d (x,a)) HdxaR).
We prove the intermediate claim HdistxS: SNo distx.
An exact proof term for the current goal is (real_SNo distx HdistxR).
We prove the intermediate claim Heps0S2: SNo eps0.
An exact proof term for the current goal is (real_SNo eps0 Heps0R).
We prove the intermediate claim Hm1S: SNo (add_SNo distx eps0).
An exact proof term for the current goal is (real_SNo (add_SNo distx eps0) (real_add_SNo distx HdistxR eps0 Heps0R)).
We prove the intermediate claim Hlt1S: apply_fun d (x,a) < add_SNo distx eps0.
An exact proof term for the current goal is (RltE_lt (apply_fun d (x,a)) (add_SNo distx eps0) Hdxalt).
We prove the intermediate claim HsumLtS: add_SNo (apply_fun d (x,y)) (apply_fun d (x,a)) < add_SNo (apply_fun d (x,y)) (add_SNo distx eps0).
An exact proof term for the current goal is (add_SNo_Lt2 (apply_fun d (x,y)) (apply_fun d (x,a)) (add_SNo distx eps0) HdxyS HdxaS Hm1S Hlt1S).
We prove the intermediate claim HrhsEq: add_SNo (apply_fun d (x,y)) (add_SNo distx eps0) = add_SNo q eps0.
We prove the intermediate claim HqDef: q = add_SNo distx (apply_fun d (x,y)).
Use reflexivity.
rewrite the current goal using HqDef (from left to right).
rewrite the current goal using (add_SNo_assoc (apply_fun d (x,y)) distx eps0 HdxyS HdistxS Heps0S2) (from left to right).
rewrite the current goal using (add_SNo_com (apply_fun d (x,y)) distx HdxyS HdistxS) (from left to right).
Use reflexivity.
We prove the intermediate claim HsumLtR: Rlt (add_SNo (apply_fun d (x,y)) (apply_fun d (x,a))) (add_SNo q eps0).
rewrite the current goal using HrhsEq (from right to left).
An exact proof term for the current goal is (RltI (add_SNo (apply_fun d (x,y)) (apply_fun d (x,a))) (add_SNo (apply_fun d (x,y)) (add_SNo distx eps0)) (real_add_SNo (apply_fun d (x,y)) HdxyR (apply_fun d (x,a)) HdxaR) (real_add_SNo (apply_fun d (x,y)) HdxyR (add_SNo distx eps0) (real_add_SNo distx HdistxR eps0 Heps0R)) HsumLtS).
An exact proof term for the current goal is (Rle_Rlt_tra_Euclid (apply_fun d (y,a)) (add_SNo (apply_fun d (x,y)) (apply_fun d (x,a))) (add_SNo q eps0) HtriLe2 HsumLtR).
We prove the intermediate claim HdistyLe: Rle disty (apply_fun d (y,a)).
An exact proof term for the current goal is (metric_dist_to_set_le_dist X d y A a Hm HyX HAsub HAne HaA).
We prove the intermediate claim HdistyLt: Rlt disty (add_SNo q eps0).
An exact proof term for the current goal is (Rle_Rlt_tra_Euclid disty (apply_fun d (y,a)) (add_SNo q eps0) HdistyLe Hdyalt).
An exact proof term for the current goal is ((not_Rlt_sym (add_SNo q eps0) disty HqepsRlt) HdistyLt).
∎