Let X, Tx, Y, dY, F, x0 and eps be given.
Assume HTx: topology_on X Tx.
Assume HdY: metric_on Y dY.
Assume HFsubC: F ⊆ continuous_function_space X Tx Y (metric_topology Y dY).
Assume Hequi: equicontinuous_family X Tx Y dY F.
Assume Hx0X: x0 ∈ X.
Assume Heps: eps ∈ R ∧ Rlt 0 eps.
Set Ty to be the term metric_topology Y dY.
Set Dom to be the term function_space X Y.
Set Tpt to be the term pointwise_convergence_topology X Tx Y Ty.
Set Spt to be the term (pointwise_subbasis X Tx Y Ty) ∪ {Dom}.
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (metric_topology_is_topology Y dY HdY).
We prove the intermediate claim HTpt: topology_on Dom Tpt.
An exact proof term for the current goal is (pointwise_convergence_topology_is_topology X Tx Y Ty HTx HTy).
We prove the intermediate claim HSpt: subbasis_on Dom Spt.
We will prove Spt ⊆ 𝒫 Dom ∧ ⋃ Spt = Dom.
Apply andI to the current goal.
Let s be given.
Assume Hs: s ∈ Spt.
We will prove s ∈ 𝒫 Dom.
Apply (binunionE' (pointwise_subbasis X Tx Y Ty) {Dom} s (s ∈ 𝒫 Dom)) to the current goal.
Assume Hsp: s ∈ pointwise_subbasis X Tx Y Ty.
An exact proof term for the current goal is (SepE1 (𝒫 Dom) (λS0 : set ⇒ ∃x U : set, x ∈ X ∧ U ∈ Ty ∧ S0 = {f ∈ Dom|apply_fun f x ∈ U}) s Hsp).
Assume HsDom: s ∈ {Dom}.
We prove the intermediate claim Hseq: s = Dom.
An exact proof term for the current goal is (SingE Dom s HsDom).
rewrite the current goal using Hseq (from left to right).
An exact proof term for the current goal is (PowerI Dom Dom (Subq_ref Dom)).
An exact proof term for the current goal is Hs.
Apply set_ext to the current goal.
Let f be given.
Assume Hf: f ∈ ⋃ Spt.
We will prove f ∈ Dom.
Apply (UnionE_impred Spt f Hf (f ∈ Dom)) to the current goal.
Let U be given.
Assume HfU: f ∈ U.
Assume HU: U ∈ Spt.
Apply (binunionE' (pointwise_subbasis X Tx Y Ty) {Dom} U (f ∈ Dom)) to the current goal.
Assume HUp: U ∈ pointwise_subbasis X Tx Y Ty.
We prove the intermediate claim HUpow: U ∈ 𝒫 Dom.
An exact proof term for the current goal is (SepE1 (𝒫 Dom) (λS0 : set ⇒ ∃x U0 : set, x ∈ X ∧ U0 ∈ Ty ∧ S0 = {f0 ∈ Dom|apply_fun f0 x ∈ U0}) U HUp).
An exact proof term for the current goal is (PowerE Dom U HUpow f HfU).
Assume HUDom: U ∈ {Dom}.
We prove the intermediate claim HUeq: U = Dom.
An exact proof term for the current goal is (SingE Dom U HUDom).
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HfU.
An exact proof term for the current goal is HU.
Let f be given.
Assume Hf: f ∈ Dom.
We prove the intermediate claim HDomInS: Dom ∈ Spt.
An exact proof term for the current goal is (binunionI2 (pointwise_subbasis X Tx Y Ty) {Dom} Dom (SingI Dom)).
An exact proof term for the current goal is (UnionI Spt f Dom Hf HDomInS).
Set delta to be the term mul_SNo eps one_third.
We prove the intermediate claim HepsR: eps ∈ R.
An exact proof term for the current goal is (andEL (eps ∈ R) (Rlt 0 eps) Heps).
We prove the intermediate claim HepsPos: Rlt 0 eps.
An exact proof term for the current goal is (andER (eps ∈ R) (Rlt 0 eps) Heps).
We prove the intermediate claim H13R: one_third ∈ R.
An exact proof term for the current goal is one_third_in_R.
We prove the intermediate claim HdeltaR: delta ∈ R.
An exact proof term for the current goal is (real_mul_SNo eps HepsR one_third H13R).
We prove the intermediate claim H13pos: Rlt 0 one_third.
An exact proof term for the current goal is (RltI 0 one_third real_0 H13R one_third_pos).
We prove the intermediate claim HdeltaPos: Rlt 0 delta.
We prove the intermediate claim HepsS: SNo eps.
An exact proof term for the current goal is (real_SNo eps HepsR).
We prove the intermediate claim H13S: SNo one_third.
An exact proof term for the current goal is (real_SNo one_third H13R).
We prove the intermediate claim H0lt_epsS: 0 < eps.
An exact proof term for the current goal is (RltE_lt 0 eps HepsPos).
We prove the intermediate claim H0lt_13S: 0 < one_third.
An exact proof term for the current goal is (RltE_lt 0 one_third H13pos).
We prove the intermediate claim H0lt_mulS: 0 < mul_SNo eps one_third.
An exact proof term for the current goal is (mul_SNo_pos_pos eps one_third HepsS H13S H0lt_epsS H0lt_13S).
An exact proof term for the current goal is (RltI 0 delta real_0 HdeltaR H0lt_mulS).
We prove the intermediate claim HequiCore: ∀x1 : set, x1 ∈ X → ∀e1 : set, e1 ∈ R ∧ Rlt 0 e1 → ∃U : set, U ∈ Tx ∧ x1 ∈ U ∧ ∀f : set, f ∈ F → ∀x : set, x ∈ X → x ∈ U → Rlt (apply_fun dY (apply_fun f x,apply_fun f x1)) e1.
Apply (and4E (topology_on X Tx) (metric_on Y dY) (F ⊆ continuous_function_space X Tx Y (metric_topology Y dY)) (∀x1 : set, x1 ∈ X → ∀e1 : set, e1 ∈ R ∧ Rlt 0 e1 → ∃U : set, U ∈ Tx ∧ x1 ∈ U ∧ ∀f : set, f ∈ F → ∀x : set, x ∈ X → x ∈ U → Rlt (apply_fun dY (apply_fun f x,apply_fun f x1)) e1) Hequi (∀x1 : set, x1 ∈ X → ∀e1 : set, e1 ∈ R ∧ Rlt 0 e1 → ∃U : set, U ∈ Tx ∧ x1 ∈ U ∧ ∀f : set, f ∈ F → ∀x : set, x ∈ X → x ∈ U → Rlt (apply_fun dY (apply_fun f x,apply_fun f x1)) e1)) to the current goal.
Assume Ht Hm Hsub Hcore.
An exact proof term for the current goal is Hcore.
We prove the intermediate claim HexU: ∃U : set, U ∈ Tx ∧ x0 ∈ U ∧ ∀f : set, f ∈ F → ∀x : set, x ∈ X → x ∈ U → Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) delta.
An exact proof term for the current goal is (HequiCore x0 Hx0X delta (andI (delta ∈ R) (Rlt 0 delta) HdeltaR HdeltaPos)).
Apply HexU to the current goal.
Let U be given.
Assume HU.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (U ∈ Tx ∧ x0 ∈ U) (∀f : set, f ∈ F → ∀x : set, x ∈ X → x ∈ U → Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) delta) HU).
Let g be given.
Assume Hgcl: g ∈ Ascoli_g_pointwise_closure X Tx Y dY F.
Let x be given.
Assume HxX: x ∈ X.
Assume HxU: x ∈ U.
We prove the intermediate claim HgDom: g ∈ Dom.
An exact proof term for the current goal is (Ascoli_g_pointwise_closure_sub X Tx Y dY F HTpt g Hgcl).
We prove the intermediate claim HgxY: apply_fun g x ∈ Y.
An exact proof term for the current goal is ((function_on_of_function_space g X Y HgDom) x HxX).
We prove the intermediate claim Hgx0Y: apply_fun g x0 ∈ Y.
An exact proof term for the current goal is ((function_on_of_function_space g X Y HgDom) x0 Hx0X).
Set Bx to be the term open_ball Y dY (apply_fun g x) delta.
Set B0 to be the term open_ball Y dY (apply_fun g x0) delta.
We prove the intermediate claim HBxTy: Bx ∈ Ty.
An exact proof term for the current goal is (open_ball_in_metric_topology Y dY (apply_fun g x) delta HdY HgxY HdeltaPos).
We prove the intermediate claim HB0Ty: B0 ∈ Ty.
An exact proof term for the current goal is (open_ball_in_metric_topology Y dY (apply_fun g x0) delta HdY Hgx0Y HdeltaPos).
Set Sx to be the term {h ∈ function_space X Y|apply_fun h x ∈ Bx}.
Set S0 to be the term {h ∈ function_space X Y|apply_fun h x0 ∈ B0}.
We prove the intermediate claim HSxSub: Sx ∈ pointwise_subbasis X Tx Y Ty.
We prove the intermediate claim HSxSubDom: Sx ⊆ function_space X Y.
Let h be given.
Assume Hh: h ∈ Sx.
An exact proof term for the current goal is (SepE1 (function_space X Y) (λh0 : set ⇒ apply_fun h0 x ∈ Bx) h Hh).
We prove the intermediate claim HSxPow: Sx ∈ 𝒫 (function_space X Y).
An exact proof term for the current goal is (PowerI (function_space X Y) Sx HSxSubDom).
We will prove Sx ∈ {S ∈ 𝒫 (function_space X Y)|∃x1 U1 : set, x1 ∈ X ∧ U1 ∈ Ty ∧ S = {f ∈ function_space X Y|apply_fun f x1 ∈ U1}}.
Apply (SepI (𝒫 (function_space X Y)) (λS : set ⇒ ∃x1 U1 : set, x1 ∈ X ∧ U1 ∈ Ty ∧ S = {f ∈ function_space X Y|apply_fun f x1 ∈ U1}) Sx HSxPow) to the current goal.
We use x to witness the existential quantifier.
We use Bx 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 HxX.
An exact proof term for the current goal is HBxTy.
Use reflexivity.
We prove the intermediate claim HS0Sub: S0 ∈ pointwise_subbasis X Tx Y Ty.
We prove the intermediate claim HS0SubDom: S0 ⊆ function_space X Y.
Let h be given.
Assume Hh: h ∈ S0.
An exact proof term for the current goal is (SepE1 (function_space X Y) (λh0 : set ⇒ apply_fun h0 x0 ∈ B0) h Hh).
We prove the intermediate claim HS0Pow: S0 ∈ 𝒫 (function_space X Y).
An exact proof term for the current goal is (PowerI (function_space X Y) S0 HS0SubDom).
We will prove S0 ∈ {S ∈ 𝒫 (function_space X Y)|∃x1 U1 : set, x1 ∈ X ∧ U1 ∈ Ty ∧ S = {f ∈ function_space X Y|apply_fun f x1 ∈ U1}}.
Apply (SepI (𝒫 (function_space X Y)) (λS : set ⇒ ∃x1 U1 : set, x1 ∈ X ∧ U1 ∈ Ty ∧ S = {f ∈ function_space X Y|apply_fun f x1 ∈ U1}) S0 HS0Pow) to the current goal.
We use x0 to witness the existential quantifier.
We use B0 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 Hx0X.
An exact proof term for the current goal is HB0Ty.
Use reflexivity.
We prove the intermediate claim HSxIn: Sx ∈ Spt.
An exact proof term for the current goal is (binunionI1 (pointwise_subbasis X Tx Y Ty) {Dom} Sx HSxSub).
We prove the intermediate claim HS0In: S0 ∈ Spt.
An exact proof term for the current goal is (binunionI1 (pointwise_subbasis X Tx Y Ty) {Dom} S0 HS0Sub).
We prove the intermediate claim HSxOpen: Sx ∈ Tpt.
An exact proof term for the current goal is (generated_topology_from_subbasis_contains_subbasis_elem Dom Spt Sx HSpt HSxIn).
We prove the intermediate claim HS0Open: S0 ∈ Tpt.
An exact proof term for the current goal is (generated_topology_from_subbasis_contains_subbasis_elem Dom Spt S0 HSpt HS0In).
Set Vx to be the term Sx ∩ S0.
We prove the intermediate claim HVxOpen: Vx ∈ Tpt.
An exact proof term for the current goal is (topology_binintersect_closed Dom Tpt Sx S0 HTpt HSxOpen HS0Open).
We prove the intermediate claim HgInSx: g ∈ Sx.
An exact proof term for the current goal is (SepI Dom (λh0 : set ⇒ apply_fun h0 x ∈ Bx) g HgDom (center_in_open_ball Y dY (apply_fun g x) delta HdY HgxY HdeltaPos)).
We prove the intermediate claim HgInS0: g ∈ S0.
An exact proof term for the current goal is (SepI Dom (λh0 : set ⇒ apply_fun h0 x0 ∈ B0) g HgDom (center_in_open_ball Y dY (apply_fun g x0) delta HdY Hgx0Y HdeltaPos)).
We prove the intermediate claim HgInVx: g ∈ Vx.
An exact proof term for the current goal is (binintersectI Sx S0 g HgInSx HgInS0).
We prove the intermediate claim HgInCl: g ∈ closure_of Dom Tpt F.
An exact proof term for the current goal is Hgcl.
We prove the intermediate claim Hcliff: g ∈ closure_of Dom Tpt F ↔ (∀W ∈ Tpt, g ∈ W → W ∩ F ≠ Empty).
An exact proof term for the current goal is (closure_characterization Dom Tpt F g HTpt HgDom).
We prove the intermediate claim Hneigh: ∀W ∈ Tpt, g ∈ W → W ∩ F ≠ Empty.
An exact proof term for the current goal is (iffEL (g ∈ closure_of Dom Tpt F) (∀W ∈ Tpt, g ∈ W → W ∩ F ≠ Empty) Hcliff HgInCl).
We prove the intermediate claim Hmeet: Vx ∩ F ≠ Empty.
An exact proof term for the current goal is (Hneigh Vx HVxOpen HgInVx).
We prove the intermediate claim Hexf: ∃f : set, f ∈ Vx ∩ F.
An exact proof term for the current goal is (nonempty_has_element (Vx ∩ F) Hmeet).
Apply Hexf to the current goal.
Let f be given.
Assume Hf: f ∈ Vx ∩ F.
We prove the intermediate claim HfVx: f ∈ Vx.
An exact proof term for the current goal is (binintersectE1 Vx F f Hf).
We prove the intermediate claim HfF: f ∈ F.
An exact proof term for the current goal is (binintersectE2 Vx F f Hf).
We prove the intermediate claim HfSx: f ∈ Sx.
An exact proof term for the current goal is (binintersectE1 Sx S0 f HfVx).
We prove the intermediate claim HfS0: f ∈ S0.
An exact proof term for the current goal is (binintersectE2 Sx S0 f HfVx).
We prove the intermediate claim HfxInBx: apply_fun f x ∈ Bx.
An exact proof term for the current goal is (SepE2 Dom (λh0 : set ⇒ apply_fun h0 x ∈ Bx) f HfSx).
We prove the intermediate claim Hfx0InB0: apply_fun f x0 ∈ B0.
An exact proof term for the current goal is (SepE2 Dom (λh0 : set ⇒ apply_fun h0 x0 ∈ B0) f HfS0).
We prove the intermediate claim Hbound1: Rlt (apply_fun dY (apply_fun g x,apply_fun f x)) delta.
An exact proof term for the current goal is (open_ballE2 Y dY (apply_fun g x) delta (apply_fun f x) HfxInBx).
We prove the intermediate claim Hbound3raw: Rlt (apply_fun dY (apply_fun g x0,apply_fun f x0)) delta.
An exact proof term for the current goal is (open_ballE2 Y dY (apply_fun g x0) delta (apply_fun f x0) Hfx0InB0).
We prove the intermediate claim HUprop: ∀f0 : set, f0 ∈ F → ∀x1 : set, x1 ∈ X → x1 ∈ U → Rlt (apply_fun dY (apply_fun f0 x1,apply_fun f0 x0)) delta.
An exact proof term for the current goal is (andER (U ∈ Tx ∧ x0 ∈ U) (∀f0 : set, f0 ∈ F → ∀x1 : set, x1 ∈ X → x1 ∈ U → Rlt (apply_fun dY (apply_fun f0 x1,apply_fun f0 x0)) delta) HU).
We prove the intermediate claim Hbound2: Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) delta.
An exact proof term for the current goal is (HUprop f HfF x HxX HxU).
We prove the intermediate claim HfDom: f ∈ Dom.
An exact proof term for the current goal is (continuous_function_space_sub X Tx Y Ty f (HFsubC f HfF)).
We prove the intermediate claim HfyY: apply_fun f x ∈ Y.
An exact proof term for the current goal is ((function_on_of_function_space f X Y HfDom) x HxX).
We prove the intermediate claim Hfy0Y: apply_fun f x0 ∈ Y.
An exact proof term for the current goal is ((function_on_of_function_space f X Y HfDom) x0 Hx0X).
We prove the intermediate claim Hsym3: apply_fun dY (apply_fun f x0,apply_fun g x0) = apply_fun dY (apply_fun g x0,apply_fun f x0).
An exact proof term for the current goal is (metric_on_symmetric Y dY (apply_fun f x0) (apply_fun g x0) HdY Hfy0Y Hgx0Y).
We prove the intermediate claim Hbound3: Rlt (apply_fun dY (apply_fun f x0,apply_fun g x0)) delta.
rewrite the current goal using Hsym3 (from left to right).
An exact proof term for the current goal is Hbound3raw.
We prove the intermediate claim Htri1: Rle (apply_fun dY (apply_fun g x,apply_fun g x0)) (add_SNo (apply_fun dY (apply_fun g x,apply_fun f x)) (apply_fun dY (apply_fun f x,apply_fun g x0))).
An exact proof term for the current goal is (metric_triangle_Rle Y dY (apply_fun g x) (apply_fun f x) (apply_fun g x0) HdY HgxY HfyY Hgx0Y).
We prove the intermediate claim Htri2: Rle (apply_fun dY (apply_fun f x,apply_fun g x0)) (add_SNo (apply_fun dY (apply_fun f x,apply_fun f x0)) (apply_fun dY (apply_fun f x0,apply_fun g x0))).
An exact proof term for the current goal is (metric_triangle_Rle Y dY (apply_fun f x) (apply_fun f x0) (apply_fun g x0) HdY HfyY Hfy0Y Hgx0Y).
We prove the intermediate claim Hd1R: apply_fun dY (apply_fun g x,apply_fun f x) ∈ R.
An exact proof term for the current goal is ((metric_on_function_on Y dY HdY) (apply_fun g x,apply_fun f x) (tuple_2_setprod_by_pair_Sigma Y Y (apply_fun g x) (apply_fun f x) HgxY HfyY)).
We prove the intermediate claim Hd2R: apply_fun dY (apply_fun f x,apply_fun f x0) ∈ R.
An exact proof term for the current goal is ((metric_on_function_on Y dY HdY) (apply_fun f x,apply_fun f x0) (tuple_2_setprod_by_pair_Sigma Y Y (apply_fun f x) (apply_fun f x0) HfyY Hfy0Y)).
We prove the intermediate claim Hd3R: apply_fun dY (apply_fun f x0,apply_fun g x0) ∈ R.
An exact proof term for the current goal is ((metric_on_function_on Y dY HdY) (apply_fun f x0,apply_fun g x0) (tuple_2_setprod_by_pair_Sigma Y Y (apply_fun f x0) (apply_fun g x0) Hfy0Y Hgx0Y)).
We prove the intermediate claim HmidR: add_SNo (apply_fun dY (apply_fun f x,apply_fun f x0)) (apply_fun dY (apply_fun f x0,apply_fun g x0)) ∈ R.
An exact proof term for the current goal is (real_add_SNo (apply_fun dY (apply_fun f x,apply_fun f x0)) Hd2R (apply_fun dY (apply_fun f x0,apply_fun g x0)) Hd3R).
We prove the intermediate claim HlhsR: add_SNo (apply_fun dY (apply_fun g x,apply_fun f x)) (add_SNo (apply_fun dY (apply_fun f x,apply_fun f x0)) (apply_fun dY (apply_fun f x0,apply_fun g x0))) ∈ R.
An exact proof term for the current goal is (real_add_SNo (apply_fun dY (apply_fun g x,apply_fun f x)) Hd1R (add_SNo (apply_fun dY (apply_fun f x,apply_fun f x0)) (apply_fun dY (apply_fun f x0,apply_fun g x0))) HmidR).
We prove the intermediate claim Htri2': Rle (add_SNo (apply_fun dY (apply_fun g x,apply_fun f x)) (apply_fun dY (apply_fun f x,apply_fun g x0))) (add_SNo (apply_fun dY (apply_fun g x,apply_fun f x)) (add_SNo (apply_fun dY (apply_fun f x,apply_fun f x0)) (apply_fun dY (apply_fun f x0,apply_fun g x0)))).
An exact proof term for the current goal is (Rle_add_SNo_2 (apply_fun dY (apply_fun g x,apply_fun f x)) (apply_fun dY (apply_fun f x,apply_fun g x0)) (add_SNo (apply_fun dY (apply_fun f x,apply_fun f x0)) (apply_fun dY (apply_fun f x0,apply_fun g x0))) Hd1R ((metric_on_function_on Y dY HdY) (apply_fun f x,apply_fun g x0) (tuple_2_setprod_by_pair_Sigma Y Y (apply_fun f x) (apply_fun g x0) HfyY Hgx0Y)) HmidR Htri2).
We prove the intermediate claim Hle3: Rle (apply_fun dY (apply_fun g x,apply_fun g x0)) (add_SNo (apply_fun dY (apply_fun g x,apply_fun f x)) (add_SNo (apply_fun dY (apply_fun f x,apply_fun f x0)) (apply_fun dY (apply_fun f x0,apply_fun g x0)))).
An exact proof term for the current goal is (Rle_tra (apply_fun dY (apply_fun g x,apply_fun g x0)) (add_SNo (apply_fun dY (apply_fun g x,apply_fun f x)) (apply_fun dY (apply_fun f x,apply_fun g x0))) (add_SNo (apply_fun dY (apply_fun g x,apply_fun f x)) (add_SNo (apply_fun dY (apply_fun f x,apply_fun f x0)) (apply_fun dY (apply_fun f x0,apply_fun g x0)))) Htri1 Htri2').
We prove the intermediate claim Hlt23: Rlt (add_SNo (apply_fun dY (apply_fun f x,apply_fun f x0)) (apply_fun dY (apply_fun f x0,apply_fun g x0))) (add_SNo delta delta).
An exact proof term for the current goal is (Rlt_add_SNo (apply_fun dY (apply_fun f x,apply_fun f x0)) delta (apply_fun dY (apply_fun f x0,apply_fun g x0)) delta Hbound2 Hbound3).
We prove the intermediate claim Hsumlt: Rlt (add_SNo (apply_fun dY (apply_fun g x,apply_fun f x)) (add_SNo (apply_fun dY (apply_fun f x,apply_fun f x0)) (apply_fun dY (apply_fun f x0,apply_fun g x0)))) (add_SNo delta (add_SNo delta delta)).
An exact proof term for the current goal is (Rlt_add_SNo (apply_fun dY (apply_fun g x,apply_fun f x)) delta (add_SNo (apply_fun dY (apply_fun f x,apply_fun f x0)) (apply_fun dY (apply_fun f x0,apply_fun g x0))) (add_SNo delta delta) Hbound1 Hlt23).
We prove the intermediate claim HdeltaS: SNo delta.
An exact proof term for the current goal is (real_SNo delta HdeltaR).
We prove the intermediate claim HepsS: SNo eps.
An exact proof term for the current goal is (real_SNo eps HepsR).
We prove the intermediate claim H13S: SNo one_third.
An exact proof term for the current goal is (real_SNo one_third H13R).
We prove the intermediate claim HsumEq: add_SNo delta (add_SNo delta delta) = eps.
rewrite the current goal using (add_SNo_assoc delta delta delta HdeltaS HdeltaS HdeltaS) (from left to right) at position 1.
We prove the intermediate claim Hdef23: two_thirds = add_SNo one_third one_third.
Use reflexivity.
We prove the intermediate claim H23R: two_thirds ∈ R.
An exact proof term for the current goal is two_thirds_in_R.
We prove the intermediate claim H23S: SNo two_thirds.
An exact proof term for the current goal is (real_SNo two_thirds H23R).
rewrite the current goal using (mul_SNo_distrL eps one_third one_third HepsS H13S H13S) (from right to left) at position 1.
rewrite the current goal using Hdef23 (from right to left) at position 1.
rewrite the current goal using (mul_SNo_distrL eps two_thirds one_third HepsS H23S H13S) (from right to left) at position 1.
rewrite the current goal using (add_SNo_com two_thirds one_third H23S H13S) (from left to right) at position 1.
rewrite the current goal using add_one_third_two_thirds_eq_1 (from left to right) at position 1.
An exact proof term for the current goal is (mul_SNo_oneR eps HepsS).
We prove the intermediate claim HsumltEps: Rlt (add_SNo (apply_fun dY (apply_fun g x,apply_fun f x)) (add_SNo (apply_fun dY (apply_fun f x,apply_fun f x0)) (apply_fun dY (apply_fun f x0,apply_fun g x0)))) eps.
rewrite the current goal using HsumEq (from right to left).
An exact proof term for the current goal is Hsumlt.
An exact proof term for the current goal is (Rle_Rlt_tra (apply_fun dY (apply_fun g x,apply_fun g x0)) (add_SNo (apply_fun dY (apply_fun g x,apply_fun f x)) (add_SNo (apply_fun dY (apply_fun f x,apply_fun f x0)) (apply_fun dY (apply_fun f x0,apply_fun g x0)))) eps Hle3 HsumltEps).
∎