Let Y, d, b and p be given.
Assume Hd: metric_on_total Y d.
Assume HbR: b ∈ R.
Assume Hp: p ∈ preimage_of (setprod Y Y) d (open_ray_lower R b).
We prove the intermediate claim HpDom: p ∈ setprod Y Y.
An exact proof term for the current goal is (SepE1 (setprod Y Y) (λq : set ⇒ apply_fun d q ∈ open_ray_lower R b) p Hp).
Set dp to be the term apply_fun d p.
We prove the intermediate claim HdpRay: dp ∈ open_ray_lower R b.
An exact proof term for the current goal is (SepE2 (setprod Y Y) (λq : set ⇒ apply_fun d q ∈ open_ray_lower R b) p Hp).
We prove the intermediate claim HrayDef: open_ray_lower R b = {x ∈ R|order_rel R x b}.
Use reflexivity.
We prove the intermediate claim HdpRay': dp ∈ {x ∈ R|order_rel R x b}.
rewrite the current goal using HrayDef (from right to left).
An exact proof term for the current goal is HdpRay.
We prove the intermediate claim HdpR: dp ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ order_rel R x0 b) dp HdpRay').
We prove the intermediate claim Hdprel: order_rel R dp b.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R x0 b) dp HdpRay').
We prove the intermediate claim Hlt: Rlt dp b.
An exact proof term for the current goal is (order_rel_R_implies_Rlt dp b Hdprel).
We prove the intermediate claim Hp0Y: p 0 ∈ Y.
An exact proof term for the current goal is (ap0_Sigma Y (λ_ : set ⇒ Y) p HpDom).
We prove the intermediate claim Hp1Y: p 1 ∈ Y.
An exact proof term for the current goal is (ap1_Sigma Y (λ_ : set ⇒ Y) p HpDom).
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 HdpS: SNo dp.
An exact proof term for the current goal is (real_SNo dp HdpR).
We prove the intermediate claim HmdpR: minus_SNo dp ∈ R.
An exact proof term for the current goal is (real_minus_SNo dp HdpR).
We prove the intermediate claim HmdpS: SNo (minus_SNo dp).
An exact proof term for the current goal is (real_SNo (minus_SNo dp) HmdpR).
Set dgap to be the term add_SNo (minus_SNo dp) b.
We prove the intermediate claim HdgapR: dgap ∈ R.
An exact proof term for the current goal is (real_add_SNo (minus_SNo dp) HmdpR b HbR).
We prove the intermediate claim HltS: dp < b.
An exact proof term for the current goal is (RltE_lt dp b Hlt).
We prove the intermediate claim HsumLt: add_SNo (minus_SNo dp) dp < add_SNo (minus_SNo dp) b.
An exact proof term for the current goal is (add_SNo_Lt2 (minus_SNo dp) dp b HmdpS HdpS HbS HltS).
We prove the intermediate claim HgapPosS: 0 < dgap.
rewrite the current goal using (add_SNo_minus_SNo_linv dp HdpS) (from right to left) at position 1.
An exact proof term for the current goal is HsumLt.
We prove the intermediate claim HgapPos: Rlt 0 dgap.
An exact proof term for the current goal is (RltI 0 dgap real_0 HdgapR HgapPosS).
Apply (exists_eps_lt_pos_Euclid dgap HdgapR HgapPos) 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 < dgap) HNpair).
We prove the intermediate claim HepsNlt: eps_ N < dgap.
An exact proof term for the current goal is (andER (N ∈ ω) (eps_ N < dgap) HNpair).
Set r to be the term eps_ (ordsucc N).
We prove the intermediate claim HsuccO: ordsucc N ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N HNomega).
We prove the intermediate claim HrR: r ∈ R.
An exact proof term for the current goal is (SNoS_omega_real r (SNo_eps_SNoS_omega (ordsucc N) HsuccO)).
We prove the intermediate claim HrS: SNo r.
An exact proof term for the current goal is (real_SNo r HrR).
We prove the intermediate claim H0ltr: 0 < r.
An exact proof term for the current goal is (SNo_eps_pos (ordsucc N) HsuccO).
We prove the intermediate claim HrPos: Rlt 0 r.
An exact proof term for the current goal is (RltI 0 r real_0 HrR H0ltr).
We prove the intermediate claim HrHalf: add_SNo r r = eps_ N.
An exact proof term for the current goal is (eps_ordsucc_half_add N (omega_nat_p N HNomega)).
We prove the intermediate claim HepsS: SNo (eps_ N).
An exact proof term for the current goal is (SNo_eps_ N HNomega).
We prove the intermediate claim HdgapS: SNo dgap.
An exact proof term for the current goal is (real_SNo dgap HdgapR).
We prove the intermediate claim HtmpLt: add_SNo dp (eps_ N) < add_SNo dp dgap.
An exact proof term for the current goal is (add_SNo_Lt2 dp (eps_ N) dgap HdpS HepsS HdgapS HepsNlt).
We prove the intermediate claim Hdeq: add_SNo dp dgap = b.
We prove the intermediate claim HdgapDef: dgap = add_SNo (minus_SNo dp) b.
Use reflexivity.
rewrite the current goal using HdgapDef (from left to right).
rewrite the current goal using (add_SNo_assoc dp (minus_SNo dp) b HdpS HmdpS HbS) (from left to right).
rewrite the current goal using (add_SNo_minus_SNo_rinv dp HdpS) (from left to right).
An exact proof term for the current goal is (add_SNo_0L b HbS).
We prove the intermediate claim HdpepsLt: add_SNo dp (eps_ N) < b.
rewrite the current goal using Hdeq (from right to left).
An exact proof term for the current goal is HtmpLt.
We prove the intermediate claim HdrLt: add_SNo dp (add_SNo r r) < b.
rewrite the current goal using HrHalf (from left to right).
An exact proof term for the current goal is HdpepsLt.
We use r 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 HrR.
An exact proof term for the current goal is HrPos.
We will prove rectangle_set (open_ball Y d (p 0) r) (open_ball Y d (p 1) r) ⊆ preimage_of (setprod Y Y) d (open_ray_lower R b).
Let q be given.
Assume HqRect: q ∈ rectangle_set (open_ball Y d (p 0) r) (open_ball Y d (p 1) r).
We prove the intermediate claim HqProd: q ∈ setprod (open_ball Y d (p 0) r) (open_ball Y d (p 1) r).
We will prove q ∈ setprod (open_ball Y d (p 0) r) (open_ball Y d (p 1) r).
rewrite the current goal using (rectangle_set_def (open_ball Y d (p 0) r) (open_ball Y d (p 1) r)) (from right to left).
An exact proof term for the current goal is HqRect.
We prove the intermediate claim HsubU: open_ball Y d (p 0) r ⊆ Y.
An exact proof term for the current goal is (open_ball_subset_X Y d (p 0) r).
We prove the intermediate claim HsubV: open_ball Y d (p 1) r ⊆ Y.
An exact proof term for the current goal is (open_ball_subset_X Y d (p 1) r).
We prove the intermediate claim HqDom: q ∈ setprod Y Y.
An exact proof term for the current goal is ((setprod_Subq (open_ball Y d (p 0) r) (open_ball Y d (p 1) r) Y Y HsubU HsubV) q HqProd).
We will prove q ∈ preimage_of (setprod Y Y) d (open_ray_lower R b).
We prove the intermediate claim HpreDef: preimage_of (setprod Y Y) d (open_ray_lower R b) = {x ∈ setprod Y Y|apply_fun d x ∈ open_ray_lower R b}.
Use reflexivity.
rewrite the current goal using HpreDef (from left to right).
Apply (SepI (setprod Y Y) (λq0 : set ⇒ apply_fun d q0 ∈ open_ray_lower R b) q HqDom) to the current goal.
We will prove apply_fun d q ∈ open_ray_lower R b.
Set dq to be the term apply_fun d q.
We prove the intermediate claim Hm: metric_on Y d.
An exact proof term for the current goal is (metric_on_total_imp_metric_on Y d Hd).
We prove the intermediate claim Hfun: function_on d (setprod Y Y) R.
An exact proof term for the current goal is (metric_on_function_on Y d Hm).
We prove the intermediate claim HdqR: dq ∈ R.
An exact proof term for the current goal is (Hfun q HqDom).
We prove the intermediate claim HdpDef: dp = apply_fun d p.
Use reflexivity.
We prove the intermediate claim HdpEta: dp = apply_fun d (p 0,p 1).
rewrite the current goal using HdpDef (from left to right).
rewrite the current goal using (setprod_eta Y Y p HpDom) (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim HetaQ: q = (q 0,q 1).
An exact proof term for the current goal is (setprod_eta (open_ball Y d (p 0) r) (open_ball Y d (p 1) r) q HqProd).
We prove the intermediate claim HdqEta: dq = apply_fun d (q 0,q 1).
We prove the intermediate claim HdqDef: dq = apply_fun d q.
Use reflexivity.
rewrite the current goal using HdqDef (from left to right).
rewrite the current goal using HetaQ (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using HrayDef (from left to right).
Apply (SepI R (λx0 : set ⇒ order_rel R x0 b) dq HdqR) to the current goal.
We will prove order_rel R dq b.
Apply (Rlt_implies_order_rel_R dq b) to the current goal.
We prove the intermediate claim Hq0Ball: q 0 ∈ open_ball Y d (p 0) r.
An exact proof term for the current goal is (ap0_Sigma (open_ball Y d (p 0) r) (λ_ : set ⇒ open_ball Y d (p 1) r) q HqProd).
We prove the intermediate claim Hq1Ball: q 1 ∈ open_ball Y d (p 1) r.
An exact proof term for the current goal is (ap1_Sigma (open_ball Y d (p 0) r) (λ_ : set ⇒ open_ball Y d (p 1) r) q HqProd).
We prove the intermediate claim Hq0Y: q 0 ∈ Y.
An exact proof term for the current goal is (open_ballE1 Y d (p 0) r (q 0) Hq0Ball).
We prove the intermediate claim Hq1Y: q 1 ∈ Y.
An exact proof term for the current goal is (open_ballE1 Y d (p 1) r (q 1) Hq1Ball).
We prove the intermediate claim HxRlt0: Rlt (apply_fun d (p 0,q 0)) r.
An exact proof term for the current goal is (open_ballE2 Y d (p 0) r (q 0) Hq0Ball).
We prove the intermediate claim HzRlt: Rlt (apply_fun d (p 1,q 1)) r.
An exact proof term for the current goal is (open_ballE2 Y d (p 1) r (q 1) Hq1Ball).
We prove the intermediate claim HsymX: apply_fun d (p 0,q 0) = apply_fun d (q 0,p 0).
An exact proof term for the current goal is (metric_on_symmetric Y d (p 0) (q 0) Hm Hp0Y Hq0Y).
We prove the intermediate claim HxRlt: Rlt (apply_fun d (q 0,p 0)) r.
rewrite the current goal using HsymX (from right to left).
An exact proof term for the current goal is HxRlt0.
We prove the intermediate claim HxR: apply_fun d (q 0,p 0) ∈ R.
An exact proof term for the current goal is (Hfun (q 0,p 0) (tuple_2_setprod_by_pair_Sigma Y Y (q 0) (p 0) Hq0Y Hp0Y)).
We prove the intermediate claim HyR: apply_fun d (q 0,q 1) ∈ R.
An exact proof term for the current goal is (Hfun (q 0,q 1) (tuple_2_setprod_by_pair_Sigma Y Y (q 0) (q 1) Hq0Y Hq1Y)).
We prove the intermediate claim HzR: apply_fun d (p 1,q 1) ∈ R.
An exact proof term for the current goal is (Hfun (p 1,q 1) (tuple_2_setprod_by_pair_Sigma Y Y (p 1) (q 1) Hp1Y Hq1Y)).
We prove the intermediate claim HrLeX: Rle (apply_fun d (q 0,p 0)) r.
An exact proof term for the current goal is (Rlt_implies_Rle (apply_fun d (q 0,p 0)) r HxRlt).
We prove the intermediate claim HrLeZ: Rle (apply_fun d (p 1,q 1)) r.
An exact proof term for the current goal is (Rlt_implies_Rle (apply_fun d (p 1,q 1)) r HzRlt).
We prove the intermediate claim Htri1: Rle (apply_fun d (q 0,q 1)) (add_SNo (apply_fun d (q 0,p 0)) (apply_fun d (p 0,q 1))).
An exact proof term for the current goal is (metric_triangle_Rle Y d (q 0) (p 0) (q 1) Hm Hq0Y Hp0Y Hq1Y).
We prove the intermediate claim Htri2: Rle (apply_fun d (p 0,q 1)) (add_SNo (apply_fun d (p 0,p 1)) (apply_fun d (p 1,q 1))).
An exact proof term for the current goal is (metric_triangle_Rle Y d (p 0) (p 1) (q 1) Hm Hp0Y Hp1Y Hq1Y).
We prove the intermediate claim Htri2dp: Rle (apply_fun d (p 0,q 1)) (add_SNo dp (apply_fun d (p 1,q 1))).
rewrite the current goal using HdpEta (from left to right).
An exact proof term for the current goal is Htri2.
We prove the intermediate claim Hlift: Rle (add_SNo (apply_fun d (q 0,p 0)) (apply_fun d (p 0,q 1))) (add_SNo (apply_fun d (q 0,p 0)) (add_SNo dp (apply_fun d (p 1,q 1)))).
An exact proof term for the current goal is (Rle_add_SNo_2 (apply_fun d (q 0,p 0)) (apply_fun d (p 0,q 1)) (add_SNo dp (apply_fun d (p 1,q 1))) HxR (Hfun (p 0,q 1) (tuple_2_setprod_by_pair_Sigma Y Y (p 0) (q 1) Hp0Y Hq1Y)) (real_add_SNo dp HdpR (apply_fun d (p 1,q 1)) HzR) Htri2dp).
We prove the intermediate claim HdqLe0: Rle (apply_fun d (q 0,q 1)) (add_SNo (apply_fun d (q 0,p 0)) (add_SNo dp (apply_fun d (p 1,q 1)))).
An exact proof term for the current goal is (Rle_tra (apply_fun d (q 0,q 1)) (add_SNo (apply_fun d (q 0,p 0)) (apply_fun d (p 0,q 1))) (add_SNo (apply_fun d (q 0,p 0)) (add_SNo dp (apply_fun d (p 1,q 1)))) Htri1 Hlift).
We prove the intermediate claim HdqLe0': Rle dq (add_SNo (apply_fun d (q 0,p 0)) (add_SNo dp (apply_fun d (p 1,q 1)))).
rewrite the current goal using HdqEta (from left to right).
An exact proof term for the current goal is HdqLe0.
We prove the intermediate claim HdpzLe: Rle (add_SNo dp (apply_fun d (p 1,q 1))) (add_SNo dp r).
An exact proof term for the current goal is (Rle_add_SNo_2 dp (apply_fun d (p 1,q 1)) r HdpR HzR HrR HrLeZ).
We prove the intermediate claim Hsum1: Rle (add_SNo (apply_fun d (q 0,p 0)) (add_SNo dp (apply_fun d (p 1,q 1)))) (add_SNo (apply_fun d (q 0,p 0)) (add_SNo dp r)).
An exact proof term for the current goal is (Rle_add_SNo_2 (apply_fun d (q 0,p 0)) (add_SNo dp (apply_fun d (p 1,q 1))) (add_SNo dp r) HxR (real_add_SNo dp HdpR (apply_fun d (p 1,q 1)) HzR) (real_add_SNo dp HdpR r HrR) HdpzLe).
We prove the intermediate claim HdqLe1: Rle dq (add_SNo (apply_fun d (q 0,p 0)) (add_SNo dp r)).
An exact proof term for the current goal is (Rle_tra dq (add_SNo (apply_fun d (q 0,p 0)) (add_SNo dp (apply_fun d (p 1,q 1)))) (add_SNo (apply_fun d (q 0,p 0)) (add_SNo dp r)) HdqLe0' Hsum1).
We prove the intermediate claim HcomX: add_SNo (apply_fun d (q 0,p 0)) (add_SNo dp r) = add_SNo (add_SNo dp r) (apply_fun d (q 0,p 0)).
An exact proof term for the current goal is (add_SNo_com (apply_fun d (q 0,p 0)) (add_SNo dp r) (real_SNo (apply_fun d (q 0,p 0)) HxR) (real_SNo (add_SNo dp r) (real_add_SNo dp HdpR r HrR))).
We prove the intermediate claim HmidLe: Rle (add_SNo (apply_fun d (q 0,p 0)) (add_SNo dp r)) (add_SNo (add_SNo dp r) r).
rewrite the current goal using HcomX (from left to right).
An exact proof term for the current goal is (Rle_add_SNo_2 (add_SNo dp r) (apply_fun d (q 0,p 0)) r (real_add_SNo dp HdpR r HrR) HxR HrR HrLeX).
We prove the intermediate claim HdqLe2: Rle dq (add_SNo (add_SNo dp r) r).
An exact proof term for the current goal is (Rle_tra dq (add_SNo (apply_fun d (q 0,p 0)) (add_SNo dp r)) (add_SNo (add_SNo dp r) r) HdqLe1 HmidLe).
We prove the intermediate claim Hassoc: add_SNo (add_SNo dp r) r = add_SNo dp (add_SNo r r).
rewrite the current goal using (add_SNo_assoc dp r r HdpS HrS HrS) (from right to left).
Use reflexivity.
We prove the intermediate claim HdqLeFinal: Rle dq (add_SNo dp (add_SNo r r)).
rewrite the current goal using Hassoc (from right to left).
An exact proof term for the current goal is HdqLe2.
We prove the intermediate claim HsumR: add_SNo dp (add_SNo r r) ∈ R.
An exact proof term for the current goal is (real_add_SNo dp HdpR (add_SNo r r) (real_add_SNo r HrR r HrR)).
We prove the intermediate claim HsumRlt: Rlt (add_SNo dp (add_SNo r r)) b.
An exact proof term for the current goal is (RltI (add_SNo dp (add_SNo r r)) b HsumR HbR HdrLt).
An exact proof term for the current goal is (Rle_Rlt_tra dq (add_SNo dp (add_SNo r r)) b HdqLeFinal HsumRlt).
∎