Let X, d, c1, c2, x, r1 and r2 be given.
Assume Hm: metric_on X d.
Assume Hc1: c1 ∈ X.
Assume Hc2: c2 ∈ X.
Assume HxX: x ∈ X.
Assume Hr1R: r1 ∈ R.
Assume Hr2R: r2 ∈ R.
Assume Hr1pos: Rlt 0 r1.
Assume Hr2pos: Rlt 0 r2.
Assume HxB1: x ∈ open_ball X d c1 r1.
Assume HxB2: x ∈ open_ball X d c2 r2.
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 Hc1xIn: (c1,x) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X c1 x Hc1 HxX).
We prove the intermediate claim Hc2xIn: (c2,x) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X c2 x Hc2 HxX).
Set dx1 to be the term apply_fun d (c1,x).
Set dx2 to be the term apply_fun d (c2,x).
We prove the intermediate claim Hdx1R: dx1 ∈ R.
An exact proof term for the current goal is (Hfun (c1,x) Hc1xIn).
We prove the intermediate claim Hdx2R: dx2 ∈ R.
An exact proof term for the current goal is (Hfun (c2,x) Hc2xIn).
We prove the intermediate claim Hdx1S: SNo dx1.
An exact proof term for the current goal is (real_SNo dx1 Hdx1R).
We prove the intermediate claim Hdx2S: SNo dx2.
An exact proof term for the current goal is (real_SNo dx2 Hdx2R).
We prove the intermediate claim Hr1S: SNo r1.
An exact proof term for the current goal is (real_SNo r1 Hr1R).
We prove the intermediate claim Hr2S: SNo r2.
An exact proof term for the current goal is (real_SNo r2 Hr2R).
We prove the intermediate claim Hdx1lt_r1: dx1 < r1.
An exact proof term for the current goal is (RltE_lt dx1 r1 (open_ballE2 X d c1 r1 x HxB1)).
We prove the intermediate claim Hdx2lt_r2: dx2 < r2.
An exact proof term for the current goal is (RltE_lt dx2 r2 (open_ballE2 X d c2 r2 x HxB2)).
Set mdx1 to be the term minus_SNo dx1.
Set mdx2 to be the term minus_SNo dx2.
We prove the intermediate claim Hmdx1Def: mdx1 = minus_SNo dx1.
Use reflexivity.
We prove the intermediate claim Hmdx2Def: mdx2 = minus_SNo dx2.
Use reflexivity.
We prove the intermediate claim Hmdx1R: mdx1 ∈ R.
An exact proof term for the current goal is (real_minus_SNo dx1 Hdx1R).
We prove the intermediate claim Hmdx2R: mdx2 ∈ R.
An exact proof term for the current goal is (real_minus_SNo dx2 Hdx2R).
We prove the intermediate claim Hmdx1S: SNo mdx1.
An exact proof term for the current goal is (real_SNo mdx1 Hmdx1R).
We prove the intermediate claim Hmdx2S: SNo mdx2.
An exact proof term for the current goal is (real_SNo mdx2 Hmdx2R).
Set delta1 to be the term add_SNo r1 mdx1.
Set delta2 to be the term add_SNo r2 mdx2.
We prove the intermediate claim Hdelta1Def: delta1 = add_SNo r1 mdx1.
Use reflexivity.
We prove the intermediate claim Hdelta2Def: delta2 = add_SNo r2 mdx2.
Use reflexivity.
We prove the intermediate claim Hdelta1R: delta1 ∈ R.
An exact proof term for the current goal is (real_add_SNo r1 Hr1R mdx1 Hmdx1R).
We prove the intermediate claim Hdelta2R: delta2 ∈ R.
An exact proof term for the current goal is (real_add_SNo r2 Hr2R mdx2 Hmdx2R).
We prove the intermediate claim Hdelta1S: SNo delta1.
An exact proof term for the current goal is (real_SNo delta1 Hdelta1R).
We prove the intermediate claim Hdelta2S: SNo delta2.
An exact proof term for the current goal is (real_SNo delta2 Hdelta2R).
We prove the intermediate claim H0lt_delta1: 0 < delta1.
rewrite the current goal using Hdelta1Def (from left to right).
rewrite the current goal using Hmdx1Def (from left to right).
We prove the intermediate claim H0plus: add_SNo 0 dx1 < r1.
rewrite the current goal using (add_SNo_0L dx1 Hdx1S) (from left to right).
An exact proof term for the current goal is Hdx1lt_r1.
An exact proof term for the current goal is (add_SNo_minus_Lt2b r1 dx1 0 Hr1S Hdx1S SNo_0 H0plus).
We prove the intermediate claim H0lt_delta2: 0 < delta2.
rewrite the current goal using Hdelta2Def (from left to right).
rewrite the current goal using Hmdx2Def (from left to right).
We prove the intermediate claim H0plus: add_SNo 0 dx2 < r2.
rewrite the current goal using (add_SNo_0L dx2 Hdx2S) (from left to right).
An exact proof term for the current goal is Hdx2lt_r2.
An exact proof term for the current goal is (add_SNo_minus_Lt2b r2 dx2 0 Hr2S Hdx2S SNo_0 H0plus).
We prove the intermediate claim Hdelta1pos: Rlt 0 delta1.
An exact proof term for the current goal is (RltI 0 delta1 real_0 Hdelta1R H0lt_delta1).
We prove the intermediate claim Hdelta2pos: Rlt 0 delta2.
An exact proof term for the current goal is (RltI 0 delta2 real_0 Hdelta2R H0lt_delta2).
Apply (SNoLt_trichotomy_or_impred delta1 delta2 Hdelta1S Hdelta2S (∃r3 : set, r3 ∈ R ∧ Rlt 0 r3 ∧ open_ball X d x r3 ⊆ (open_ball X d c1 r1) ∩ (open_ball X d c2 r2))) to the current goal.
Assume Hdelta1lt: delta1 < delta2.
We prove the intermediate claim HexN: ∃N ∈ ω, eps_ N < delta1.
An exact proof term for the current goal is (exists_eps_lt_pos delta1 Hdelta1R Hdelta1pos).
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 < delta1) HNpair).
We prove the intermediate claim HepsLt1: eps_ N < delta1.
An exact proof term for the current goal is (andER (N ∈ ω) (eps_ N < delta1) HNpair).
Set r3 to be the term eps_ N.
We prove the intermediate claim Hr3S: SNo r3.
An exact proof term for the current goal is (SNo_eps_ N HNomega).
We prove the intermediate claim Hr3InS: r3 ∈ SNoS_ ω.
An exact proof term for the current goal is (SNo_eps_SNoS_omega N HNomega).
We prove the intermediate claim Hr3R: r3 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real r3 Hr3InS).
We prove the intermediate claim H0lt_r3: 0 < r3.
An exact proof term for the current goal is (SNo_eps_pos N HNomega).
We prove the intermediate claim Hr3pos: Rlt 0 r3.
An exact proof term for the current goal is (RltI 0 r3 real_0 Hr3R H0lt_r3).
We prove the intermediate claim Hr3lt1: r3 < delta1.
An exact proof term for the current goal is HepsLt1.
We prove the intermediate claim Hr3lt2: r3 < delta2.
An exact proof term for the current goal is (SNoLt_tra r3 delta1 delta2 Hr3S Hdelta1S Hdelta2S Hr3lt1 Hdelta1lt).
We use r3 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hr3R.
An exact proof term for the current goal is Hr3pos.
Let y be given.
Assume Hy: y ∈ open_ball X d x r3.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (open_ballE1 X d x r3 y Hy).
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 Hc1yIn: (c1,y) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X c1 y Hc1 HyX).
We prove the intermediate claim Hc2yIn: (c2,y) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X c2 y Hc2 HyX).
Set dxy to be the term apply_fun d (x,y).
Set dc1y to be the term apply_fun d (c1,y).
Set dc2y to be the term apply_fun d (c2,y).
We prove the intermediate claim HdxyR: dxy ∈ R.
An exact proof term for the current goal is (Hfun (x,y) HxyIn).
We prove the intermediate claim Hdc1yR: dc1y ∈ R.
An exact proof term for the current goal is (Hfun (c1,y) Hc1yIn).
We prove the intermediate claim Hdc2yR: dc2y ∈ R.
An exact proof term for the current goal is (Hfun (c2,y) Hc2yIn).
We prove the intermediate claim HdxyS: SNo dxy.
An exact proof term for the current goal is (real_SNo dxy HdxyR).
We prove the intermediate claim Hdc1yS: SNo dc1y.
An exact proof term for the current goal is (real_SNo dc1y Hdc1yR).
We prove the intermediate claim Hdc2yS: SNo dc2y.
An exact proof term for the current goal is (real_SNo dc2y Hdc2yR).
We prove the intermediate claim HdxyLtR3: dxy < r3.
An exact proof term for the current goal is (RltE_lt dxy r3 (open_ballE2 X d x r3 y Hy)).
We prove the intermediate claim Hsum1R: add_SNo dx1 dxy ∈ R.
An exact proof term for the current goal is (real_add_SNo dx1 Hdx1R dxy HdxyR).
We prove the intermediate claim Hsum2R: add_SNo dx2 dxy ∈ R.
An exact proof term for the current goal is (real_add_SNo dx2 Hdx2R dxy HdxyR).
We prove the intermediate claim Hsum1S: SNo (add_SNo dx1 dxy).
An exact proof term for the current goal is (real_SNo (add_SNo dx1 dxy) Hsum1R).
We prove the intermediate claim Hsum2S: SNo (add_SNo dx2 dxy).
An exact proof term for the current goal is (real_SNo (add_SNo dx2 dxy) Hsum2R).
We prove the intermediate claim Hdx1r3R: add_SNo dx1 r3 ∈ R.
An exact proof term for the current goal is (real_add_SNo dx1 Hdx1R r3 Hr3R).
We prove the intermediate claim Hdx2r3R: add_SNo dx2 r3 ∈ R.
An exact proof term for the current goal is (real_add_SNo dx2 Hdx2R r3 Hr3R).
We prove the intermediate claim Hdx1r3S: SNo (add_SNo dx1 r3).
An exact proof term for the current goal is (real_SNo (add_SNo dx1 r3) Hdx1r3R).
We prove the intermediate claim Hdx2r3S: SNo (add_SNo dx2 r3).
An exact proof term for the current goal is (real_SNo (add_SNo dx2 r3) Hdx2r3R).
We prove the intermediate claim Hdx1delta1R: add_SNo dx1 delta1 ∈ R.
An exact proof term for the current goal is (real_add_SNo dx1 Hdx1R delta1 Hdelta1R).
We prove the intermediate claim Hdx2delta2R: add_SNo dx2 delta2 ∈ R.
An exact proof term for the current goal is (real_add_SNo dx2 Hdx2R delta2 Hdelta2R).
We prove the intermediate claim Hdx1delta1S: SNo (add_SNo dx1 delta1).
An exact proof term for the current goal is (real_SNo (add_SNo dx1 delta1) Hdx1delta1R).
We prove the intermediate claim Hdx2delta2S: SNo (add_SNo dx2 delta2).
An exact proof term for the current goal is (real_SNo (add_SNo dx2 delta2) Hdx2delta2R).
We prove the intermediate claim Hdx1r3lt: add_SNo dx1 r3 < r1.
We prove the intermediate claim Hdx1r3lt': add_SNo dx1 r3 < add_SNo dx1 delta1.
An exact proof term for the current goal is (add_SNo_Lt2 dx1 r3 delta1 Hdx1S Hr3S Hdelta1S Hr3lt1).
We prove the intermediate claim Heq: add_SNo dx1 delta1 = r1.
We prove the intermediate claim Hcom: add_SNo dx1 delta1 = add_SNo delta1 dx1.
An exact proof term for the current goal is (add_SNo_com dx1 delta1 Hdx1S Hdelta1S).
rewrite the current goal using Hcom (from left to right).
rewrite the current goal using (add_SNo_minus_R2' r1 dx1 Hr1S Hdx1S) (from left to right).
Use reflexivity.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hdx1r3lt'.
We prove the intermediate claim Hdx2r3lt: add_SNo dx2 r3 < r2.
We prove the intermediate claim Hdx2r3lt': add_SNo dx2 r3 < add_SNo dx2 delta2.
An exact proof term for the current goal is (add_SNo_Lt2 dx2 r3 delta2 Hdx2S Hr3S Hdelta2S Hr3lt2).
We prove the intermediate claim Heq: add_SNo dx2 delta2 = r2.
We prove the intermediate claim Hcom: add_SNo dx2 delta2 = add_SNo delta2 dx2.
An exact proof term for the current goal is (add_SNo_com dx2 delta2 Hdx2S Hdelta2S).
rewrite the current goal using Hcom (from left to right).
rewrite the current goal using (add_SNo_minus_R2' r2 dx2 Hr2S Hdx2S) (from left to right).
Use reflexivity.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hdx2r3lt'.
We prove the intermediate claim Hsum1lt: add_SNo dx1 dxy < r1.
We prove the intermediate claim Hlt1: add_SNo dx1 dxy < add_SNo dx1 r3.
An exact proof term for the current goal is (add_SNo_Lt2 dx1 dxy r3 Hdx1S HdxyS Hr3S HdxyLtR3).
An exact proof term for the current goal is (SNoLt_tra (add_SNo dx1 dxy) (add_SNo dx1 r3) r1 Hsum1S Hdx1r3S Hr1S Hlt1 Hdx1r3lt).
We prove the intermediate claim Hsum2lt: add_SNo dx2 dxy < r2.
We prove the intermediate claim Hlt1: add_SNo dx2 dxy < add_SNo dx2 r3.
An exact proof term for the current goal is (add_SNo_Lt2 dx2 dxy r3 Hdx2S HdxyS Hr3S HdxyLtR3).
An exact proof term for the current goal is (SNoLt_tra (add_SNo dx2 dxy) (add_SNo dx2 r3) r2 Hsum2S Hdx2r3S Hr2S Hlt1 Hdx2r3lt).
We prove the intermediate claim Htri1: Rle dc1y (add_SNo dx1 dxy).
An exact proof term for the current goal is (metric_triangle_Rle X d c1 x y Hm Hc1 HxX HyX).
We prove the intermediate claim Htri2: Rle dc2y (add_SNo dx2 dxy).
An exact proof term for the current goal is (metric_triangle_Rle X d c2 x y Hm Hc2 HxX HyX).
We prove the intermediate claim Hsum1Rlt: Rlt (add_SNo dx1 dxy) r1.
An exact proof term for the current goal is (RltI (add_SNo dx1 dxy) r1 Hsum1R Hr1R Hsum1lt).
We prove the intermediate claim Hsum2Rlt: Rlt (add_SNo dx2 dxy) r2.
An exact proof term for the current goal is (RltI (add_SNo dx2 dxy) r2 Hsum2R Hr2R Hsum2lt).
We prove the intermediate claim Hdc1yRlt: Rlt dc1y r1.
An exact proof term for the current goal is (Rle_Rlt_tra dc1y (add_SNo dx1 dxy) r1 Htri1 Hsum1Rlt).
We prove the intermediate claim Hdc2yRlt: Rlt dc2y r2.
An exact proof term for the current goal is (Rle_Rlt_tra dc2y (add_SNo dx2 dxy) r2 Htri2 Hsum2Rlt).
We prove the intermediate claim HyB1: y ∈ open_ball X d c1 r1.
An exact proof term for the current goal is (open_ballI X d c1 r1 y HyX Hdc1yRlt).
We prove the intermediate claim HyB2: y ∈ open_ball X d c2 r2.
An exact proof term for the current goal is (open_ballI X d c2 r2 y HyX Hdc2yRlt).
Apply binintersectI to the current goal.
An exact proof term for the current goal is HyB1.
An exact proof term for the current goal is HyB2.
Assume Hdeltaeq: delta1 = delta2.
We prove the intermediate claim HexN: ∃N ∈ ω, eps_ N < delta2.
An exact proof term for the current goal is (exists_eps_lt_pos delta2 Hdelta2R Hdelta2pos).
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 < delta2) HNpair).
We prove the intermediate claim HepsLt2: eps_ N < delta2.
An exact proof term for the current goal is (andER (N ∈ ω) (eps_ N < delta2) HNpair).
Set r3 to be the term eps_ N.
We prove the intermediate claim Hr3S: SNo r3.
An exact proof term for the current goal is (SNo_eps_ N HNomega).
We prove the intermediate claim Hr3InS: r3 ∈ SNoS_ ω.
An exact proof term for the current goal is (SNo_eps_SNoS_omega N HNomega).
We prove the intermediate claim Hr3R: r3 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real r3 Hr3InS).
We prove the intermediate claim H0lt_r3: 0 < r3.
An exact proof term for the current goal is (SNo_eps_pos N HNomega).
We prove the intermediate claim Hr3pos: Rlt 0 r3.
An exact proof term for the current goal is (RltI 0 r3 real_0 Hr3R H0lt_r3).
We prove the intermediate claim Hr3lt2: r3 < delta2.
An exact proof term for the current goal is HepsLt2.
We prove the intermediate claim Hr3lt1: r3 < delta1.
rewrite the current goal using Hdeltaeq (from left to right).
An exact proof term for the current goal is Hr3lt2.
We use r3 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hr3R.
An exact proof term for the current goal is Hr3pos.
Let y be given.
Assume Hy: y ∈ open_ball X d x r3.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (open_ballE1 X d x r3 y Hy).
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 Hc1yIn: (c1,y) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X c1 y Hc1 HyX).
We prove the intermediate claim Hc2yIn: (c2,y) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X c2 y Hc2 HyX).
Set dxy to be the term apply_fun d (x,y).
Set dc1y to be the term apply_fun d (c1,y).
Set dc2y to be the term apply_fun d (c2,y).
We prove the intermediate claim HdxyR: dxy ∈ R.
An exact proof term for the current goal is (Hfun (x,y) HxyIn).
We prove the intermediate claim Hdc1yR: dc1y ∈ R.
An exact proof term for the current goal is (Hfun (c1,y) Hc1yIn).
We prove the intermediate claim Hdc2yR: dc2y ∈ R.
An exact proof term for the current goal is (Hfun (c2,y) Hc2yIn).
We prove the intermediate claim HdxyS: SNo dxy.
An exact proof term for the current goal is (real_SNo dxy HdxyR).
We prove the intermediate claim Hdc1yS: SNo dc1y.
An exact proof term for the current goal is (real_SNo dc1y Hdc1yR).
We prove the intermediate claim Hdc2yS: SNo dc2y.
An exact proof term for the current goal is (real_SNo dc2y Hdc2yR).
We prove the intermediate claim HdxyLtR3: dxy < r3.
An exact proof term for the current goal is (RltE_lt dxy r3 (open_ballE2 X d x r3 y Hy)).
We prove the intermediate claim Hsum1R: add_SNo dx1 dxy ∈ R.
An exact proof term for the current goal is (real_add_SNo dx1 Hdx1R dxy HdxyR).
We prove the intermediate claim Hsum2R: add_SNo dx2 dxy ∈ R.
An exact proof term for the current goal is (real_add_SNo dx2 Hdx2R dxy HdxyR).
We prove the intermediate claim Hsum1S: SNo (add_SNo dx1 dxy).
An exact proof term for the current goal is (real_SNo (add_SNo dx1 dxy) Hsum1R).
We prove the intermediate claim Hsum2S: SNo (add_SNo dx2 dxy).
An exact proof term for the current goal is (real_SNo (add_SNo dx2 dxy) Hsum2R).
We prove the intermediate claim Hdx1r3R: add_SNo dx1 r3 ∈ R.
An exact proof term for the current goal is (real_add_SNo dx1 Hdx1R r3 Hr3R).
We prove the intermediate claim Hdx2r3R: add_SNo dx2 r3 ∈ R.
An exact proof term for the current goal is (real_add_SNo dx2 Hdx2R r3 Hr3R).
We prove the intermediate claim Hdx1r3S: SNo (add_SNo dx1 r3).
An exact proof term for the current goal is (real_SNo (add_SNo dx1 r3) Hdx1r3R).
We prove the intermediate claim Hdx2r3S: SNo (add_SNo dx2 r3).
An exact proof term for the current goal is (real_SNo (add_SNo dx2 r3) Hdx2r3R).
We prove the intermediate claim Hdx1r3lt: add_SNo dx1 r3 < r1.
We prove the intermediate claim Hdx1r3lt': add_SNo dx1 r3 < add_SNo dx1 delta1.
An exact proof term for the current goal is (add_SNo_Lt2 dx1 r3 delta1 Hdx1S Hr3S Hdelta1S Hr3lt1).
We prove the intermediate claim Heq: add_SNo dx1 delta1 = r1.
We prove the intermediate claim Hcom: add_SNo dx1 delta1 = add_SNo delta1 dx1.
An exact proof term for the current goal is (add_SNo_com dx1 delta1 Hdx1S Hdelta1S).
rewrite the current goal using Hcom (from left to right).
rewrite the current goal using (add_SNo_minus_R2' r1 dx1 Hr1S Hdx1S) (from left to right).
Use reflexivity.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hdx1r3lt'.
We prove the intermediate claim Hdx2r3lt: add_SNo dx2 r3 < r2.
We prove the intermediate claim Hdx2r3lt': add_SNo dx2 r3 < add_SNo dx2 delta2.
An exact proof term for the current goal is (add_SNo_Lt2 dx2 r3 delta2 Hdx2S Hr3S Hdelta2S Hr3lt2).
We prove the intermediate claim Heq: add_SNo dx2 delta2 = r2.
We prove the intermediate claim Hcom: add_SNo dx2 delta2 = add_SNo delta2 dx2.
An exact proof term for the current goal is (add_SNo_com dx2 delta2 Hdx2S Hdelta2S).
rewrite the current goal using Hcom (from left to right).
rewrite the current goal using (add_SNo_minus_R2' r2 dx2 Hr2S Hdx2S) (from left to right).
Use reflexivity.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hdx2r3lt'.
We prove the intermediate claim Hsum1lt: add_SNo dx1 dxy < r1.
We prove the intermediate claim Hlt1: add_SNo dx1 dxy < add_SNo dx1 r3.
An exact proof term for the current goal is (add_SNo_Lt2 dx1 dxy r3 Hdx1S HdxyS Hr3S HdxyLtR3).
An exact proof term for the current goal is (SNoLt_tra (add_SNo dx1 dxy) (add_SNo dx1 r3) r1 Hsum1S Hdx1r3S Hr1S Hlt1 Hdx1r3lt).
We prove the intermediate claim Hsum2lt: add_SNo dx2 dxy < r2.
We prove the intermediate claim Hlt1: add_SNo dx2 dxy < add_SNo dx2 r3.
An exact proof term for the current goal is (add_SNo_Lt2 dx2 dxy r3 Hdx2S HdxyS Hr3S HdxyLtR3).
An exact proof term for the current goal is (SNoLt_tra (add_SNo dx2 dxy) (add_SNo dx2 r3) r2 Hsum2S Hdx2r3S Hr2S Hlt1 Hdx2r3lt).
We prove the intermediate claim Htri1: Rle dc1y (add_SNo dx1 dxy).
An exact proof term for the current goal is (metric_triangle_Rle X d c1 x y Hm Hc1 HxX HyX).
We prove the intermediate claim Htri2: Rle dc2y (add_SNo dx2 dxy).
An exact proof term for the current goal is (metric_triangle_Rle X d c2 x y Hm Hc2 HxX HyX).
We prove the intermediate claim Hsum1Rlt: Rlt (add_SNo dx1 dxy) r1.
An exact proof term for the current goal is (RltI (add_SNo dx1 dxy) r1 Hsum1R Hr1R Hsum1lt).
We prove the intermediate claim Hsum2Rlt: Rlt (add_SNo dx2 dxy) r2.
An exact proof term for the current goal is (RltI (add_SNo dx2 dxy) r2 Hsum2R Hr2R Hsum2lt).
We prove the intermediate claim Hdc1yRlt: Rlt dc1y r1.
An exact proof term for the current goal is (Rle_Rlt_tra dc1y (add_SNo dx1 dxy) r1 Htri1 Hsum1Rlt).
We prove the intermediate claim Hdc2yRlt: Rlt dc2y r2.
An exact proof term for the current goal is (Rle_Rlt_tra dc2y (add_SNo dx2 dxy) r2 Htri2 Hsum2Rlt).
We prove the intermediate claim HyB1: y ∈ open_ball X d c1 r1.
An exact proof term for the current goal is (open_ballI X d c1 r1 y HyX Hdc1yRlt).
We prove the intermediate claim HyB2: y ∈ open_ball X d c2 r2.
An exact proof term for the current goal is (open_ballI X d c2 r2 y HyX Hdc2yRlt).
Apply binintersectI to the current goal.
An exact proof term for the current goal is HyB1.
An exact proof term for the current goal is HyB2.
Assume Hdelta2lt: delta2 < delta1.
We prove the intermediate claim HexN: ∃N ∈ ω, eps_ N < delta2.
An exact proof term for the current goal is (exists_eps_lt_pos delta2 Hdelta2R Hdelta2pos).
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 < delta2) HNpair).
We prove the intermediate claim HepsLt2: eps_ N < delta2.
An exact proof term for the current goal is (andER (N ∈ ω) (eps_ N < delta2) HNpair).
Set r3 to be the term eps_ N.
We prove the intermediate claim Hr3S: SNo r3.
An exact proof term for the current goal is (SNo_eps_ N HNomega).
We prove the intermediate claim Hr3InS: r3 ∈ SNoS_ ω.
An exact proof term for the current goal is (SNo_eps_SNoS_omega N HNomega).
We prove the intermediate claim Hr3R: r3 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real r3 Hr3InS).
We prove the intermediate claim H0lt_r3: 0 < r3.
An exact proof term for the current goal is (SNo_eps_pos N HNomega).
We prove the intermediate claim Hr3pos: Rlt 0 r3.
An exact proof term for the current goal is (RltI 0 r3 real_0 Hr3R H0lt_r3).
We prove the intermediate claim Hr3lt2: r3 < delta2.
An exact proof term for the current goal is HepsLt2.
We prove the intermediate claim Hr3lt1: r3 < delta1.
An exact proof term for the current goal is (SNoLt_tra r3 delta2 delta1 Hr3S Hdelta2S Hdelta1S Hr3lt2 Hdelta2lt).
We use r3 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hr3R.
An exact proof term for the current goal is Hr3pos.
Let y be given.
Assume Hy: y ∈ open_ball X d x r3.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (open_ballE1 X d x r3 y Hy).
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 Hc1yIn: (c1,y) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X c1 y Hc1 HyX).
We prove the intermediate claim Hc2yIn: (c2,y) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X c2 y Hc2 HyX).
Set dxy to be the term apply_fun d (x,y).
Set dc1y to be the term apply_fun d (c1,y).
Set dc2y to be the term apply_fun d (c2,y).
We prove the intermediate claim HdxyR: dxy ∈ R.
An exact proof term for the current goal is (Hfun (x,y) HxyIn).
We prove the intermediate claim Hdc1yR: dc1y ∈ R.
An exact proof term for the current goal is (Hfun (c1,y) Hc1yIn).
We prove the intermediate claim Hdc2yR: dc2y ∈ R.
An exact proof term for the current goal is (Hfun (c2,y) Hc2yIn).
We prove the intermediate claim HdxyS: SNo dxy.
An exact proof term for the current goal is (real_SNo dxy HdxyR).
We prove the intermediate claim Hdc1yS: SNo dc1y.
An exact proof term for the current goal is (real_SNo dc1y Hdc1yR).
We prove the intermediate claim Hdc2yS: SNo dc2y.
An exact proof term for the current goal is (real_SNo dc2y Hdc2yR).
We prove the intermediate claim HdxyLtR3: dxy < r3.
An exact proof term for the current goal is (RltE_lt dxy r3 (open_ballE2 X d x r3 y Hy)).
We prove the intermediate claim Hsum1R: add_SNo dx1 dxy ∈ R.
An exact proof term for the current goal is (real_add_SNo dx1 Hdx1R dxy HdxyR).
We prove the intermediate claim Hsum2R: add_SNo dx2 dxy ∈ R.
An exact proof term for the current goal is (real_add_SNo dx2 Hdx2R dxy HdxyR).
We prove the intermediate claim Hsum1S: SNo (add_SNo dx1 dxy).
An exact proof term for the current goal is (real_SNo (add_SNo dx1 dxy) Hsum1R).
We prove the intermediate claim Hsum2S: SNo (add_SNo dx2 dxy).
An exact proof term for the current goal is (real_SNo (add_SNo dx2 dxy) Hsum2R).
We prove the intermediate claim Hdx1r3R: add_SNo dx1 r3 ∈ R.
An exact proof term for the current goal is (real_add_SNo dx1 Hdx1R r3 Hr3R).
We prove the intermediate claim Hdx2r3R: add_SNo dx2 r3 ∈ R.
An exact proof term for the current goal is (real_add_SNo dx2 Hdx2R r3 Hr3R).
We prove the intermediate claim Hdx1r3S: SNo (add_SNo dx1 r3).
An exact proof term for the current goal is (real_SNo (add_SNo dx1 r3) Hdx1r3R).
We prove the intermediate claim Hdx2r3S: SNo (add_SNo dx2 r3).
An exact proof term for the current goal is (real_SNo (add_SNo dx2 r3) Hdx2r3R).
We prove the intermediate claim Hdx1r3lt: add_SNo dx1 r3 < r1.
We prove the intermediate claim Hdx1r3lt': add_SNo dx1 r3 < add_SNo dx1 delta1.
An exact proof term for the current goal is (add_SNo_Lt2 dx1 r3 delta1 Hdx1S Hr3S Hdelta1S Hr3lt1).
We prove the intermediate claim Heq: add_SNo dx1 delta1 = r1.
We prove the intermediate claim Hcom: add_SNo dx1 delta1 = add_SNo delta1 dx1.
An exact proof term for the current goal is (add_SNo_com dx1 delta1 Hdx1S Hdelta1S).
rewrite the current goal using Hcom (from left to right).
rewrite the current goal using (add_SNo_minus_R2' r1 dx1 Hr1S Hdx1S) (from left to right).
Use reflexivity.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hdx1r3lt'.
We prove the intermediate claim Hdx2r3lt: add_SNo dx2 r3 < r2.
We prove the intermediate claim Hdx2r3lt': add_SNo dx2 r3 < add_SNo dx2 delta2.
An exact proof term for the current goal is (add_SNo_Lt2 dx2 r3 delta2 Hdx2S Hr3S Hdelta2S Hr3lt2).
We prove the intermediate claim Heq: add_SNo dx2 delta2 = r2.
We prove the intermediate claim Hcom: add_SNo dx2 delta2 = add_SNo delta2 dx2.
An exact proof term for the current goal is (add_SNo_com dx2 delta2 Hdx2S Hdelta2S).
rewrite the current goal using Hcom (from left to right).
rewrite the current goal using (add_SNo_minus_R2' r2 dx2 Hr2S Hdx2S) (from left to right).
Use reflexivity.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hdx2r3lt'.
We prove the intermediate claim Hsum1lt: add_SNo dx1 dxy < r1.
We prove the intermediate claim Hlt1: add_SNo dx1 dxy < add_SNo dx1 r3.
An exact proof term for the current goal is (add_SNo_Lt2 dx1 dxy r3 Hdx1S HdxyS Hr3S HdxyLtR3).
An exact proof term for the current goal is (SNoLt_tra (add_SNo dx1 dxy) (add_SNo dx1 r3) r1 Hsum1S Hdx1r3S Hr1S Hlt1 Hdx1r3lt).
We prove the intermediate claim Hsum2lt: add_SNo dx2 dxy < r2.
We prove the intermediate claim Hlt1: add_SNo dx2 dxy < add_SNo dx2 r3.
An exact proof term for the current goal is (add_SNo_Lt2 dx2 dxy r3 Hdx2S HdxyS Hr3S HdxyLtR3).
An exact proof term for the current goal is (SNoLt_tra (add_SNo dx2 dxy) (add_SNo dx2 r3) r2 Hsum2S Hdx2r3S Hr2S Hlt1 Hdx2r3lt).
We prove the intermediate claim Htri1: Rle dc1y (add_SNo dx1 dxy).
An exact proof term for the current goal is (metric_triangle_Rle X d c1 x y Hm Hc1 HxX HyX).
We prove the intermediate claim Htri2: Rle dc2y (add_SNo dx2 dxy).
An exact proof term for the current goal is (metric_triangle_Rle X d c2 x y Hm Hc2 HxX HyX).
We prove the intermediate claim Hsum1Rlt: Rlt (add_SNo dx1 dxy) r1.
An exact proof term for the current goal is (RltI (add_SNo dx1 dxy) r1 Hsum1R Hr1R Hsum1lt).
We prove the intermediate claim Hsum2Rlt: Rlt (add_SNo dx2 dxy) r2.
An exact proof term for the current goal is (RltI (add_SNo dx2 dxy) r2 Hsum2R Hr2R Hsum2lt).
We prove the intermediate claim Hdc1yRlt: Rlt dc1y r1.
An exact proof term for the current goal is (Rle_Rlt_tra dc1y (add_SNo dx1 dxy) r1 Htri1 Hsum1Rlt).
We prove the intermediate claim Hdc2yRlt: Rlt dc2y r2.
An exact proof term for the current goal is (Rle_Rlt_tra dc2y (add_SNo dx2 dxy) r2 Htri2 Hsum2Rlt).
We prove the intermediate claim HyB1: y ∈ open_ball X d c1 r1.
An exact proof term for the current goal is (open_ballI X d c1 r1 y HyX Hdc1yRlt).
We prove the intermediate claim HyB2: y ∈ open_ball X d c2 r2.
An exact proof term for the current goal is (open_ballI X d c2 r2 y HyX Hdc2yRlt).
Apply binintersectI to the current goal.
An exact proof term for the current goal is HyB1.
An exact proof term for the current goal is HyB2.
∎