Let Y, d, a and p be given.
Assume Hd: metric_on_total Y d.
Assume HaR: a ∈ R.
Assume Hp: p ∈ preimage_of (setprod Y Y) d (open_ray_upper R a).
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_upper R a) p Hp).
Set dp to be the term apply_fun d p.
We prove the intermediate claim HdpRay: dp ∈ open_ray_upper R a.
An exact proof term for the current goal is (SepE2 (setprod Y Y) (λq : set ⇒ apply_fun d q ∈ open_ray_upper R a) p Hp).
We prove the intermediate claim HrayDef: open_ray_upper R a = {x ∈ R|order_rel R a x}.
Use reflexivity.
We prove the intermediate claim HdpRay': dp ∈ {x ∈ R|order_rel R a x}.
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 a x0) dp HdpRay').
We prove the intermediate claim Hdprel: order_rel R a dp.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R a x0) dp HdpRay').
We prove the intermediate claim Hlt: Rlt a dp.
An exact proof term for the current goal is (order_rel_R_implies_Rlt a dp 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 HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
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 HmaR: minus_SNo a ∈ R.
An exact proof term for the current goal is (real_minus_SNo a HaR).
We prove the intermediate claim HmaS: SNo (minus_SNo a).
An exact proof term for the current goal is (real_SNo (minus_SNo a) HmaR).
Set dgap to be the term add_SNo (minus_SNo a) dp.
We prove the intermediate claim HdgapR: dgap ∈ R.
An exact proof term for the current goal is (real_add_SNo (minus_SNo a) HmaR dp HdpR).
We prove the intermediate claim HltS: a < dp.
An exact proof term for the current goal is (RltE_lt a dp Hlt).
We prove the intermediate claim HsumLt: add_SNo (minus_SNo a) a < add_SNo (minus_SNo a) dp.
An exact proof term for the current goal is (add_SNo_Lt2 (minus_SNo a) a dp HmaS HaS HdpS HltS).
We prove the intermediate claim HgapPosS: 0 < dgap.
rewrite the current goal using (add_SNo_minus_SNo_linv a HaS) (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 a (eps_ N) < add_SNo a dgap.
An exact proof term for the current goal is (add_SNo_Lt2 a (eps_ N) dgap HaS HepsS HdgapS HepsNlt).
We prove the intermediate claim Haeq: add_SNo a dgap = dp.
We prove the intermediate claim HdgapDef: dgap = add_SNo (minus_SNo a) dp.
Use reflexivity.
rewrite the current goal using HdgapDef (from left to right).
rewrite the current goal using (add_SNo_assoc a (minus_SNo a) dp HaS HmaS HdpS) (from left to right).
rewrite the current goal using (add_SNo_minus_SNo_rinv a HaS) (from left to right).
An exact proof term for the current goal is (add_SNo_0L dp HdpS).
We prove the intermediate claim HaepsLt: add_SNo a (eps_ N) < dp.
rewrite the current goal using Haeq (from right to left).
An exact proof term for the current goal is HtmpLt.
We prove the intermediate claim HarLt: add_SNo a (add_SNo r r) < dp.
rewrite the current goal using HrHalf (from left to right).
An exact proof term for the current goal is HaepsLt.
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_upper R a).
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_upper R a).
We prove the intermediate claim HpreDef: preimage_of (setprod Y Y) d (open_ray_upper R a) = {x ∈ setprod Y Y|apply_fun d x ∈ open_ray_upper R a}.
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_upper R a) q HqDom) to the current goal.
We will prove apply_fun d q ∈ open_ray_upper R a.
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 a x0) dq HdqR) to the current goal.
We will prove order_rel R a dq.
Apply (Rlt_implies_order_rel_R a dq) to the current goal.
Apply (dneg (Rlt a dq)) to the current goal.
Assume Hn: ¬ (Rlt a dq).
We will prove False.
We prove the intermediate claim HdqLeA: Rle dq a.
An exact proof term for the current goal is (RleI dq a HdqR HaR Hn).
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 HxRlt: 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 HyRle: Rle (apply_fun d (q 0,q 1)) a.
rewrite the current goal using HdqEta (from right to left).
An exact proof term for the current goal is HdqLeA.
We prove the intermediate claim HzRlt0: 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 HsymZ: apply_fun d (p 1,q 1) = apply_fun d (q 1,p 1).
An exact proof term for the current goal is (metric_on_symmetric Y d (p 1) (q 1) Hm Hp1Y Hq1Y).
We prove the intermediate claim HzRlt: Rlt (apply_fun d (q 1,p 1)) r.
rewrite the current goal using HsymZ (from right to left).
An exact proof term for the current goal is HzRlt0.
We prove the intermediate claim HxR: apply_fun d (p 0,q 0) ∈ R.
An exact proof term for the current goal is (Hfun (p 0,q 0) (tuple_2_setprod_by_pair_Sigma Y Y (p 0) (q 0) Hp0Y Hq0Y)).
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 (q 1,p 1) ∈ R.
An exact proof term for the current goal is (Hfun (q 1,p 1) (tuple_2_setprod_by_pair_Sigma Y Y (q 1) (p 1) Hq1Y Hp1Y)).
We prove the intermediate claim HyzR: add_SNo (apply_fun d (q 0,q 1)) (apply_fun d (q 1,p 1)) ∈ R.
An exact proof term for the current goal is (real_add_SNo (apply_fun d (q 0,q 1)) HyR (apply_fun d (q 1,p 1)) HzR).
We prove the intermediate claim HxrR: r ∈ R.
An exact proof term for the current goal is HrR.
We prove the intermediate claim HxLeR: Rle (apply_fun d (p 0,q 0)) r.
An exact proof term for the current goal is (Rlt_implies_Rle (apply_fun d (p 0,q 0)) r HxRlt).
We prove the intermediate claim HzLeR: Rle (apply_fun d (q 1,p 1)) r.
An exact proof term for the current goal is (Rlt_implies_Rle (apply_fun d (q 1,p 1)) r HzRlt).
We prove the intermediate claim Htri1: Rle (apply_fun d (p 0,p 1)) (add_SNo (apply_fun d (p 0,q 0)) (apply_fun d (q 0,p 1))).
An exact proof term for the current goal is (metric_triangle_Rle Y d (p 0) (q 0) (p 1) Hm Hp0Y Hq0Y Hp1Y).
We prove the intermediate claim Htri1dp: Rle dp (add_SNo (apply_fun d (p 0,q 0)) (apply_fun d (q 0,p 1))).
rewrite the current goal using HdpEta (from left to right).
An exact proof term for the current goal is Htri1.
We prove the intermediate claim Htri2: Rle (apply_fun d (q 0,p 1)) (add_SNo (apply_fun d (q 0,q 1)) (apply_fun d (q 1,p 1))).
An exact proof term for the current goal is (metric_triangle_Rle Y d (q 0) (q 1) (p 1) Hm Hq0Y Hq1Y Hp1Y).
We prove the intermediate claim Hlift: Rle (add_SNo (apply_fun d (p 0,q 0)) (apply_fun d (q 0,p 1))) (add_SNo (apply_fun d (p 0,q 0)) (add_SNo (apply_fun d (q 0,q 1)) (apply_fun d (q 1,p 1)))).
An exact proof term for the current goal is (Rle_add_SNo_2 (apply_fun d (p 0,q 0)) (apply_fun d (q 0,p 1)) (add_SNo (apply_fun d (q 0,q 1)) (apply_fun d (q 1,p 1))) HxR (Hfun (q 0,p 1) (tuple_2_setprod_by_pair_Sigma Y Y (q 0) (p 1) Hq0Y Hp1Y)) HyzR Htri2).
We prove the intermediate claim HdpLeSum0: Rle dp (add_SNo (apply_fun d (p 0,q 0)) (add_SNo (apply_fun d (q 0,q 1)) (apply_fun d (q 1,p 1)))).
An exact proof term for the current goal is (Rle_tra dp (add_SNo (apply_fun d (p 0,q 0)) (apply_fun d (q 0,p 1))) (add_SNo (apply_fun d (p 0,q 0)) (add_SNo (apply_fun d (q 0,q 1)) (apply_fun d (q 1,p 1)))) Htri1dp Hlift).
We prove the intermediate claim HyzLe: Rle (add_SNo (apply_fun d (q 0,q 1)) (apply_fun d (q 1,p 1))) (add_SNo a (apply_fun d (q 1,p 1))).
We prove the intermediate claim Hcom1: add_SNo (apply_fun d (q 0,q 1)) (apply_fun d (q 1,p 1)) = add_SNo (apply_fun d (q 1,p 1)) (apply_fun d (q 0,q 1)).
An exact proof term for the current goal is (add_SNo_com (apply_fun d (q 0,q 1)) (apply_fun d (q 1,p 1)) (real_SNo (apply_fun d (q 0,q 1)) HyR) (real_SNo (apply_fun d (q 1,p 1)) HzR)).
We prove the intermediate claim Hcom2: add_SNo a (apply_fun d (q 1,p 1)) = add_SNo (apply_fun d (q 1,p 1)) a.
An exact proof term for the current goal is (add_SNo_com a (apply_fun d (q 1,p 1)) HaS (real_SNo (apply_fun d (q 1,p 1)) HzR)).
rewrite the current goal using Hcom1 (from left to right).
rewrite the current goal using Hcom2 (from left to right).
An exact proof term for the current goal is (Rle_add_SNo_2 (apply_fun d (q 1,p 1)) (apply_fun d (q 0,q 1)) a HzR HyR HaR HyRle).
We prove the intermediate claim Hsum1: Rle (add_SNo (apply_fun d (p 0,q 0)) (add_SNo (apply_fun d (q 0,q 1)) (apply_fun d (q 1,p 1)))) (add_SNo (apply_fun d (p 0,q 0)) (add_SNo a (apply_fun d (q 1,p 1)))).
An exact proof term for the current goal is (Rle_add_SNo_2 (apply_fun d (p 0,q 0)) (add_SNo (apply_fun d (q 0,q 1)) (apply_fun d (q 1,p 1))) (add_SNo a (apply_fun d (q 1,p 1))) HxR HyzR (real_add_SNo a HaR (apply_fun d (q 1,p 1)) HzR) HyzLe).
We prove the intermediate claim HdpLeSum1: Rle dp (add_SNo (apply_fun d (p 0,q 0)) (add_SNo a (apply_fun d (q 1,p 1)))).
An exact proof term for the current goal is (Rle_tra dp (add_SNo (apply_fun d (p 0,q 0)) (add_SNo (apply_fun d (q 0,q 1)) (apply_fun d (q 1,p 1)))) (add_SNo (apply_fun d (p 0,q 0)) (add_SNo a (apply_fun d (q 1,p 1)))) HdpLeSum0 Hsum1).
We prove the intermediate claim HazLe: Rle (add_SNo a (apply_fun d (q 1,p 1))) (add_SNo a r).
An exact proof term for the current goal is (Rle_add_SNo_2 a (apply_fun d (q 1,p 1)) r HaR HzR HrR HzLeR).
We prove the intermediate claim HdpLeSum2: Rle dp (add_SNo (apply_fun d (p 0,q 0)) (add_SNo a r)).
An exact proof term for the current goal is (Rle_tra dp (add_SNo (apply_fun d (p 0,q 0)) (add_SNo a (apply_fun d (q 1,p 1)))) (add_SNo (apply_fun d (p 0,q 0)) (add_SNo a r)) HdpLeSum1 (Rle_add_SNo_2 (apply_fun d (p 0,q 0)) (add_SNo a (apply_fun d (q 1,p 1))) (add_SNo a r) HxR (real_add_SNo a HaR (apply_fun d (q 1,p 1)) HzR) (real_add_SNo a HaR r HrR) HazLe)).
We prove the intermediate claim HcomX: add_SNo (apply_fun d (p 0,q 0)) (add_SNo a r) = add_SNo (add_SNo a r) (apply_fun d (p 0,q 0)).
An exact proof term for the current goal is (add_SNo_com (apply_fun d (p 0,q 0)) (add_SNo a r) (real_SNo (apply_fun d (p 0,q 0)) HxR) (real_SNo (add_SNo a r) (real_add_SNo a HaR r HrR))).
We prove the intermediate claim HdpLeSum3: Rle dp (add_SNo (add_SNo a r) r).
We prove the intermediate claim HmidLe: Rle (add_SNo (apply_fun d (p 0,q 0)) (add_SNo a r)) (add_SNo (add_SNo a 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 a r) (apply_fun d (p 0,q 0)) r (real_add_SNo a HaR r HrR) HxR HrR HxLeR).
An exact proof term for the current goal is (Rle_tra dp (add_SNo (apply_fun d (p 0,q 0)) (add_SNo a r)) (add_SNo (add_SNo a r) r) HdpLeSum2 HmidLe).
We prove the intermediate claim Hassoc: add_SNo (add_SNo a r) r = add_SNo a (add_SNo r r).
rewrite the current goal using (add_SNo_assoc a r r HaS HrS HrS) (from right to left).
Use reflexivity.
We prove the intermediate claim HdpLeFinal: Rle dp (add_SNo a (add_SNo r r)).
rewrite the current goal using Hassoc (from right to left).
An exact proof term for the current goal is HdpLeSum3.
We prove the intermediate claim HarR: add_SNo a (add_SNo r r) ∈ R.
An exact proof term for the current goal is (real_add_SNo a HaR (add_SNo r r) (real_add_SNo r HrR r HrR)).
We prove the intermediate claim HarRlt: Rlt (add_SNo a (add_SNo r r)) dp.
An exact proof term for the current goal is (RltI (add_SNo a (add_SNo r r)) dp HarR HdpR HarLt).
An exact proof term for the current goal is ((RleE_nlt dp (add_SNo a (add_SNo r r)) HdpLeFinal) HarRlt).
∎