Let X, Tx, f, g and x0 be given.
Assume HTx: topology_on X Tx.
Assume Hfcont: continuous_map X Tx R R_standard_topology f.
Assume Hgcont: continuous_map X Tx R R_standard_topology g.
Assume Hx0X: x0 ∈ X.
Assume Hfx0: apply_fun f x0 = 0.
Assume Hgx0: apply_fun g x0 = 0.
We will prove ∃h : set, continuous_map X Tx R R_standard_topology h ∧ apply_fun h x0 = 0 ∧ ∀y : set, y ∈ X → (apply_fun f y = 1 ∨ apply_fun g y = 1) → apply_fun h y = 1.
We prove the intermediate claim HfFun: function_on f X R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology f Hfcont).
We prove the intermediate claim HgFun: function_on g X R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology g Hgcont).
Set maxfg to be the term (λx : set ⇒ if (Rlt (apply_fun f x) (apply_fun g x)) then (apply_fun g x) else (apply_fun f x)).
Set h0 to be the term (λx : set ⇒ if (Rlt 1 (maxfg x)) then 1 else (maxfg x)).
Set h to be the term graph X (λx : set ⇒ h0 x).
We use h to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim Hfunh: function_on h X R.
Let x be given.
Assume HxX: x ∈ X.
rewrite the current goal using (apply_fun_graph X (λu : set ⇒ h0 u) x HxX) (from left to right).
We prove the intermediate claim HfxR: apply_fun f x ∈ R.
An exact proof term for the current goal is (HfFun x HxX).
We prove the intermediate claim HgxR: apply_fun g x ∈ R.
An exact proof term for the current goal is (HgFun x HxX).
We prove the intermediate claim HmaxR: maxfg x ∈ R.
We prove the intermediate claim Hdef: maxfg x = (if (Rlt (apply_fun f x) (apply_fun g x)) then (apply_fun g x) else (apply_fun f x)).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
Apply (xm (Rlt (apply_fun f x) (apply_fun g x))) to the current goal.
Assume Hlt: Rlt (apply_fun f x) (apply_fun g x).
rewrite the current goal using (If_i_1 (Rlt (apply_fun f x) (apply_fun g x)) (apply_fun g x) (apply_fun f x) Hlt) (from left to right).
An exact proof term for the current goal is HgxR.
Assume Hnlt: ¬ (Rlt (apply_fun f x) (apply_fun g x)).
rewrite the current goal using (If_i_0 (Rlt (apply_fun f x) (apply_fun g x)) (apply_fun g x) (apply_fun f x) Hnlt) (from left to right).
An exact proof term for the current goal is HfxR.
Apply (xm (Rlt 1 (maxfg x))) to the current goal.
Assume H1lt: Rlt 1 (maxfg x).
rewrite the current goal using (If_i_1 (Rlt 1 (maxfg x)) 1 (maxfg x) H1lt) (from left to right).
An exact proof term for the current goal is real_1.
Assume Hn1lt: ¬ (Rlt 1 (maxfg x)).
rewrite the current goal using (If_i_0 (Rlt 1 (maxfg x)) 1 (maxfg x) Hn1lt) (from left to right).
An exact proof term for the current goal is HmaxR.
Set S to be the term open_rays_subbasis R.
We prove the intermediate claim HS: subbasis_on R S.
An exact proof term for the current goal is (open_rays_subbasis_is_subbasis R).
We prove the intermediate claim Hgen: generated_topology_from_subbasis R S = R_standard_topology.
rewrite the current goal using open_rays_subbasis_for_order_topology_R (from left to right).
rewrite the current goal using standard_topology_is_order_topology (from left to right).
Use reflexivity.
rewrite the current goal using Hgen (from right to left).
Apply (continuous_map_from_subbasis X Tx R S h HTx Hfunh HS) to the current goal.
Let s be given.
Assume HsS: s ∈ S.
We will prove preimage_of X h s ∈ Tx.
Apply (binunionE' ({I ∈ 𝒫 R|∃a0 ∈ R, I = open_ray_upper R a0} ∪ {I ∈ 𝒫 R|∃b0 ∈ R, I = open_ray_lower R b0}) {R} s (preimage_of X h s ∈ Tx)) to the current goal.
Assume Hs0: s ∈ ({I ∈ 𝒫 R|∃a0 ∈ R, I = open_ray_upper R a0} ∪ {I ∈ 𝒫 R|∃b0 ∈ R, I = open_ray_lower R b0}).
Apply (binunionE' {I ∈ 𝒫 R|∃a0 ∈ R, I = open_ray_upper R a0} {I ∈ 𝒫 R|∃b0 ∈ R, I = open_ray_lower R b0} s (preimage_of X h s ∈ Tx)) to the current goal.
Assume Hsup: s ∈ {I ∈ 𝒫 R|∃a0 ∈ R, I = open_ray_upper R a0}.
We prove the intermediate claim Hexa0: ∃a0 ∈ R, s = open_ray_upper R a0.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λI0 : set ⇒ ∃a0 ∈ R, I0 = open_ray_upper R a0) s Hsup).
Apply Hexa0 to the current goal.
Let a be given.
Assume Hapack.
Apply Hapack to the current goal.
Assume HaR: a ∈ R.
Assume Hseq: s = open_ray_upper R a.
rewrite the current goal using Hseq (from left to right).
Set Uf to be the term preimage_of X f (open_ray_upper R a).
Set Ug to be the term preimage_of X g (open_ray_upper R a).
We prove the intermediate claim HopenRay: open_ray_upper R a ∈ R_standard_topology.
rewrite the current goal using standard_topology_is_order_topology (from right to left).
We prove the intermediate claim HsRay: open_ray_upper R a ∈ open_rays_subbasis R.
An exact proof term for the current goal is (open_ray_upper_in_open_rays_subbasis R a HaR).
An exact proof term for the current goal is (open_rays_subbasis_sub_order_topology_R (open_ray_upper R a) HsRay).
We prove the intermediate claim HUf: Uf ∈ Tx.
An exact proof term for the current goal is (continuous_map_preimage X Tx R R_standard_topology f Hfcont (open_ray_upper R a) HopenRay).
We prove the intermediate claim HUg: Ug ∈ Tx.
An exact proof term for the current goal is (continuous_map_preimage X Tx R R_standard_topology g Hgcont (open_ray_upper R a) HopenRay).
Apply (xm (Rlt a 1)) to the current goal.
Assume Halt: Rlt a 1.
We prove the intermediate claim HpreEq: preimage_of X h (open_ray_upper R a) = Uf ∪ Ug.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ preimage_of X h (open_ray_upper R a).
We will prove x ∈ Uf ∪ Ug.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λu : set ⇒ apply_fun h u ∈ open_ray_upper R a) x Hx).
We prove the intermediate claim HhxRay: apply_fun h x ∈ open_ray_upper R a.
An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun h u ∈ open_ray_upper R a) x Hx).
We prove the intermediate claim HhxEq: apply_fun h x = h0 x.
An exact proof term for the current goal is (apply_fun_graph X (λu : set ⇒ h0 u) x HxX).
We prove the intermediate claim Hrel: order_rel R a (apply_fun h x).
An exact proof term for the current goal is (SepE2 R (λr : set ⇒ order_rel R a r) (apply_fun h x) HhxRay).
We prove the intermediate claim Halt_h: Rlt a (apply_fun h x).
An exact proof term for the current goal is (order_rel_R_implies_Rlt a (apply_fun h x) Hrel).
We prove the intermediate claim Halt_h0: Rlt a (h0 x).
rewrite the current goal using HhxEq (from right to left).
An exact proof term for the current goal is Halt_h.
We prove the intermediate claim HaxMax: Rlt a (maxfg x).
Apply (xm (Rlt 1 (maxfg x))) to the current goal.
Assume H1lt: Rlt 1 (maxfg x).
An exact proof term for the current goal is (Rlt_tra a 1 (maxfg x) Halt H1lt).
Assume Hn1lt: ¬ (Rlt 1 (maxfg x)).
We prove the intermediate claim Heq: h0 x = maxfg x.
An exact proof term for the current goal is (If_i_0 (Rlt 1 (maxfg x)) 1 (maxfg x) Hn1lt).
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is Halt_h0.
We prove the intermediate claim Hor: Rlt a (apply_fun f x) ∨ Rlt a (apply_fun g x).
Apply (xm (Rlt (apply_fun f x) (apply_fun g x))) to the current goal.
Assume Hfg: Rlt (apply_fun f x) (apply_fun g x).
We prove the intermediate claim Heq: maxfg x = apply_fun g x.
An exact proof term for the current goal is (If_i_1 (Rlt (apply_fun f x) (apply_fun g x)) (apply_fun g x) (apply_fun f x) Hfg).
We prove the intermediate claim Hag: Rlt a (apply_fun g x).
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HaxMax.
An exact proof term for the current goal is (orIR (Rlt a (apply_fun f x)) (Rlt a (apply_fun g x)) Hag).
Assume Hnfg: ¬ (Rlt (apply_fun f x) (apply_fun g x)).
We prove the intermediate claim Heq: maxfg x = apply_fun f x.
An exact proof term for the current goal is (If_i_0 (Rlt (apply_fun f x) (apply_fun g x)) (apply_fun g x) (apply_fun f x) Hnfg).
We prove the intermediate claim Haf: Rlt a (apply_fun f x).
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HaxMax.
An exact proof term for the current goal is (orIL (Rlt a (apply_fun f x)) (Rlt a (apply_fun g x)) Haf).
Apply Hor to the current goal.
Assume Haf: Rlt a (apply_fun f x).
We will prove x ∈ Uf ∪ Ug.
We prove the intermediate claim HfxR: apply_fun f x ∈ R.
An exact proof term for the current goal is (HfFun x HxX).
We prove the intermediate claim HfxRay: apply_fun f x ∈ open_ray_upper R a.
An exact proof term for the current goal is (SepI R (λr : set ⇒ order_rel R a r) (apply_fun f x) HfxR (Rlt_implies_order_rel_R a (apply_fun f x) Haf)).
We prove the intermediate claim HxUf: x ∈ Uf.
An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun f u ∈ open_ray_upper R a) x HxX HfxRay).
An exact proof term for the current goal is (binunionI1 Uf Ug x HxUf).
Assume Hag: Rlt a (apply_fun g x).
We will prove x ∈ Uf ∪ Ug.
We prove the intermediate claim HgxR: apply_fun g x ∈ R.
An exact proof term for the current goal is (HgFun x HxX).
We prove the intermediate claim HgxRay: apply_fun g x ∈ open_ray_upper R a.
An exact proof term for the current goal is (SepI R (λr : set ⇒ order_rel R a r) (apply_fun g x) HgxR (Rlt_implies_order_rel_R a (apply_fun g x) Hag)).
We prove the intermediate claim HxUg: x ∈ Ug.
An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun g u ∈ open_ray_upper R a) x HxX HgxRay).
An exact proof term for the current goal is (binunionI2 Uf Ug x HxUg).
Let x be given.
Assume Hx: x ∈ Uf ∪ Ug.
We will prove x ∈ preimage_of X h (open_ray_upper R a).
We prove the intermediate claim HxX: x ∈ X.
Apply (binunionE' Uf Ug x (x ∈ X)) to the current goal.
Assume HxUf: x ∈ Uf.
An exact proof term for the current goal is (SepE1 X (λu : set ⇒ apply_fun f u ∈ open_ray_upper R a) x HxUf).
Assume HxUg: x ∈ Ug.
An exact proof term for the current goal is (SepE1 X (λu : set ⇒ apply_fun g u ∈ open_ray_upper R a) x HxUg).
An exact proof term for the current goal is Hx.
We prove the intermediate claim Hor: Rlt a (apply_fun f x) ∨ Rlt a (apply_fun g x).
Apply (binunionE' Uf Ug x (Rlt a (apply_fun f x) ∨ Rlt a (apply_fun g x))) to the current goal.
Assume HxUf: x ∈ Uf.
We prove the intermediate claim HfxRay: apply_fun f x ∈ open_ray_upper R a.
An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun f u ∈ open_ray_upper R a) x HxUf).
We prove the intermediate claim Hrel: order_rel R a (apply_fun f x).
An exact proof term for the current goal is (SepE2 R (λr : set ⇒ order_rel R a r) (apply_fun f x) HfxRay).
An exact proof term for the current goal is (orIL (Rlt a (apply_fun f x)) (Rlt a (apply_fun g x)) (order_rel_R_implies_Rlt a (apply_fun f x) Hrel)).
Assume HxUg: x ∈ Ug.
We prove the intermediate claim HgxRay: apply_fun g x ∈ open_ray_upper R a.
An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun g u ∈ open_ray_upper R a) x HxUg).
We prove the intermediate claim Hrel: order_rel R a (apply_fun g x).
An exact proof term for the current goal is (SepE2 R (λr : set ⇒ order_rel R a r) (apply_fun g x) HgxRay).
An exact proof term for the current goal is (orIR (Rlt a (apply_fun f x)) (Rlt a (apply_fun g x)) (order_rel_R_implies_Rlt a (apply_fun g x) Hrel)).
An exact proof term for the current goal is Hx.
We prove the intermediate claim HaxMax: Rlt a (maxfg x).
Apply Hor to the current goal.
Assume Haf: Rlt a (apply_fun f x).
We will prove Rlt a (maxfg x).
Apply (xm (Rlt (apply_fun f x) (apply_fun g x))) to the current goal.
Assume Hfg: Rlt (apply_fun f x) (apply_fun g x).
We prove the intermediate claim Heq: maxfg x = apply_fun g x.
An exact proof term for the current goal is (If_i_1 (Rlt (apply_fun f x) (apply_fun g x)) (apply_fun g x) (apply_fun f x) Hfg).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (Rlt_tra a (apply_fun f x) (apply_fun g x) Haf Hfg).
Assume Hnfg: ¬ (Rlt (apply_fun f x) (apply_fun g x)).
We prove the intermediate claim Heq: maxfg x = apply_fun f x.
An exact proof term for the current goal is (If_i_0 (Rlt (apply_fun f x) (apply_fun g x)) (apply_fun g x) (apply_fun f x) Hnfg).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is Haf.
Assume Hag: Rlt a (apply_fun g x).
We will prove Rlt a (maxfg x).
Apply (xm (Rlt (apply_fun f x) (apply_fun g x))) to the current goal.
Assume Hfg: Rlt (apply_fun f x) (apply_fun g x).
We prove the intermediate claim Heq: maxfg x = apply_fun g x.
An exact proof term for the current goal is (If_i_1 (Rlt (apply_fun f x) (apply_fun g x)) (apply_fun g x) (apply_fun f x) Hfg).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is Hag.
Assume Hnfg: ¬ (Rlt (apply_fun f x) (apply_fun g x)).
We prove the intermediate claim Heq: maxfg x = apply_fun f x.
An exact proof term for the current goal is (If_i_0 (Rlt (apply_fun f x) (apply_fun g x)) (apply_fun g x) (apply_fun f x) Hnfg).
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim HgxR: apply_fun g x ∈ R.
An exact proof term for the current goal is (HgFun x HxX).
We prove the intermediate claim HfxR: apply_fun f x ∈ R.
An exact proof term for the current goal is (HfFun x HxX).
We prove the intermediate claim Hle: Rle (apply_fun g x) (apply_fun f x).
An exact proof term for the current goal is (RleI (apply_fun g x) (apply_fun f x) HgxR HfxR Hnfg).
An exact proof term for the current goal is (Rlt_Rle_tra a (apply_fun g x) (apply_fun f x) Hag Hle).
We prove the intermediate claim Himg: apply_fun h x ∈ open_ray_upper R a.
We prove the intermediate claim HhxEq: apply_fun h x = h0 x.
An exact proof term for the current goal is (apply_fun_graph X (λu : set ⇒ h0 u) x HxX).
rewrite the current goal using HhxEq (from left to right).
We prove the intermediate claim Hdef0: h0 x = (if (Rlt 1 (maxfg x)) then 1 else (maxfg x)).
Use reflexivity.
rewrite the current goal using Hdef0 (from left to right).
Apply (xm (Rlt 1 (maxfg x))) to the current goal.
Assume H1lt: Rlt 1 (maxfg x).
We prove the intermediate claim Heq: (if (Rlt 1 (maxfg x)) then 1 else (maxfg x)) = 1.
An exact proof term for the current goal is (If_i_1 (Rlt 1 (maxfg x)) 1 (maxfg x) H1lt).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (SepI R (λr : set ⇒ order_rel R a r) 1 real_1 (Rlt_implies_order_rel_R a 1 Halt)).
Assume Hn1lt: ¬ (Rlt 1 (maxfg x)).
We prove the intermediate claim Heq: (if (Rlt 1 (maxfg x)) then 1 else (maxfg x)) = (maxfg x).
An exact proof term for the current goal is (If_i_0 (Rlt 1 (maxfg x)) 1 (maxfg x) Hn1lt).
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim HmaxR: maxfg x ∈ R.
We prove the intermediate claim Hdef: maxfg x = (if (Rlt (apply_fun f x) (apply_fun g x)) then (apply_fun g x) else (apply_fun f x)).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
Apply (xm (Rlt (apply_fun f x) (apply_fun g x))) to the current goal.
Assume Hfg: Rlt (apply_fun f x) (apply_fun g x).
rewrite the current goal using (If_i_1 (Rlt (apply_fun f x) (apply_fun g x)) (apply_fun g x) (apply_fun f x) Hfg) (from left to right).
An exact proof term for the current goal is (HgFun x HxX).
Assume Hnfg: ¬ (Rlt (apply_fun f x) (apply_fun g x)).
rewrite the current goal using (If_i_0 (Rlt (apply_fun f x) (apply_fun g x)) (apply_fun g x) (apply_fun f x) Hnfg) (from left to right).
An exact proof term for the current goal is (HfFun x HxX).
An exact proof term for the current goal is (SepI R (λr : set ⇒ order_rel R a r) (maxfg x) HmaxR (Rlt_implies_order_rel_R a (maxfg x) HaxMax)).
An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun h u ∈ open_ray_upper R a) x HxX Himg).
rewrite the current goal using HpreEq (from left to right).
An exact proof term for the current goal is (topology_binunion_closed X Tx Uf Ug HTx HUf HUg).
Assume Hnalt: ¬ (Rlt a 1).
We prove the intermediate claim HpreEq: preimage_of X h (open_ray_upper R a) = Empty.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ preimage_of X h (open_ray_upper R a).
We will prove x ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λu : set ⇒ apply_fun h u ∈ open_ray_upper R a) x Hx).
We prove the intermediate claim HhxRay: apply_fun h x ∈ open_ray_upper R a.
An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun h u ∈ open_ray_upper R a) x Hx).
We prove the intermediate claim Hrel: order_rel R a (apply_fun h x).
An exact proof term for the current goal is (SepE2 R (λr : set ⇒ order_rel R a r) (apply_fun h x) HhxRay).
We prove the intermediate claim Halt_h: Rlt a (apply_fun h x).
An exact proof term for the current goal is (order_rel_R_implies_Rlt a (apply_fun h x) Hrel).
We prove the intermediate claim HhxEq: apply_fun h x = h0 x.
An exact proof term for the current goal is (apply_fun_graph X (λu : set ⇒ h0 u) x HxX).
We prove the intermediate claim Halt_h0: Rlt a (h0 x).
rewrite the current goal using HhxEq (from right to left).
An exact proof term for the current goal is Halt_h.
Apply (xm (Rlt 1 (maxfg x))) to the current goal.
Assume H1lt: Rlt 1 (maxfg x).
We prove the intermediate claim Heq: h0 x = 1.
An exact proof term for the current goal is (If_i_1 (Rlt 1 (maxfg x)) 1 (maxfg x) H1lt).
We prove the intermediate claim Halt1: Rlt a 1.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Halt_h0.
An exact proof term for the current goal is (Hnalt Halt1).
Assume Hn1lt: ¬ (Rlt 1 (maxfg x)).
We prove the intermediate claim Heq: h0 x = maxfg x.
An exact proof term for the current goal is (If_i_0 (Rlt 1 (maxfg x)) 1 (maxfg x) Hn1lt).
We prove the intermediate claim HmaxR: maxfg x ∈ R.
We prove the intermediate claim Hdef: maxfg x = (if (Rlt (apply_fun f x) (apply_fun g x)) then (apply_fun g x) else (apply_fun f x)).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
Apply (xm (Rlt (apply_fun f x) (apply_fun g x))) to the current goal.
Assume Hfg: Rlt (apply_fun f x) (apply_fun g x).
rewrite the current goal using (If_i_1 (Rlt (apply_fun f x) (apply_fun g x)) (apply_fun g x) (apply_fun f x) Hfg) (from left to right).
An exact proof term for the current goal is (HgFun x HxX).
Assume Hnfg: ¬ (Rlt (apply_fun f x) (apply_fun g x)).
rewrite the current goal using (If_i_0 (Rlt (apply_fun f x) (apply_fun g x)) (apply_fun g x) (apply_fun f x) Hnfg) (from left to right).
An exact proof term for the current goal is (HfFun x HxX).
We prove the intermediate claim Hle: Rle (maxfg x) 1.
An exact proof term for the current goal is (RleI (maxfg x) 1 HmaxR real_1 Hn1lt).
We prove the intermediate claim Halt1: Rlt a 1.
We prove the intermediate claim HaltMax: Rlt a (maxfg x).
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Halt_h0.
An exact proof term for the current goal is (Rlt_Rle_tra a (maxfg x) 1 HaltMax Hle).
An exact proof term for the current goal is (Hnalt Halt1).
Let x be given.
Assume HxE: x ∈ Empty.
An exact proof term for the current goal is (FalseE (EmptyE x HxE) (x ∈ preimage_of X h (open_ray_upper R a))).
rewrite the current goal using HpreEq (from left to right).
An exact proof term for the current goal is (topology_has_empty X Tx HTx).
Assume Hslo: s ∈ {I ∈ 𝒫 R|∃b0 ∈ R, I = open_ray_lower R b0}.
We prove the intermediate claim Hexb0: ∃b0 ∈ R, s = open_ray_lower R b0.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λI0 : set ⇒ ∃b0 ∈ R, I0 = open_ray_lower R b0) s Hslo).
Apply Hexb0 to the current goal.
Let b be given.
Assume Hbpack.
Apply Hbpack to the current goal.
Assume HbR: b ∈ R.
Assume Hseq: s = open_ray_lower R b.
rewrite the current goal using Hseq (from left to right).
Set Lf to be the term preimage_of X f (open_ray_lower R b).
Set Lg to be the term preimage_of X g (open_ray_lower R b).
We prove the intermediate claim HopenRay: open_ray_lower R b ∈ R_standard_topology.
rewrite the current goal using standard_topology_is_order_topology (from right to left).
We prove the intermediate claim HsRay: open_ray_lower R b ∈ open_rays_subbasis R.
An exact proof term for the current goal is (open_ray_lower_in_open_rays_subbasis R b HbR).
An exact proof term for the current goal is (open_rays_subbasis_sub_order_topology_R (open_ray_lower R b) HsRay).
We prove the intermediate claim HLf: Lf ∈ Tx.
An exact proof term for the current goal is (continuous_map_preimage X Tx R R_standard_topology f Hfcont (open_ray_lower R b) HopenRay).
We prove the intermediate claim HLg: Lg ∈ Tx.
An exact proof term for the current goal is (continuous_map_preimage X Tx R R_standard_topology g Hgcont (open_ray_lower R b) HopenRay).
Apply (xm (Rlt 1 b)) to the current goal.
Assume H1ltb: Rlt 1 b.
We prove the intermediate claim HpreEq: preimage_of X h (open_ray_lower R b) = X.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ preimage_of X h (open_ray_lower R b).
An exact proof term for the current goal is (SepE1 X (λu : set ⇒ apply_fun h u ∈ open_ray_lower R b) x Hx).
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim HhxRay: apply_fun h x ∈ open_ray_lower R b.
We prove the intermediate claim HhxEq: apply_fun h x = h0 x.
An exact proof term for the current goal is (apply_fun_graph X (λu : set ⇒ h0 u) x HxX).
rewrite the current goal using HhxEq (from left to right).
We prove the intermediate claim Hdef0: h0 x = (if (Rlt 1 (maxfg x)) then 1 else (maxfg x)).
Use reflexivity.
rewrite the current goal using Hdef0 (from left to right).
Apply (xm (Rlt 1 (maxfg x))) to the current goal.
Assume H1lt: Rlt 1 (maxfg x).
We prove the intermediate claim Heq: (if (Rlt 1 (maxfg x)) then 1 else (maxfg x)) = 1.
An exact proof term for the current goal is (If_i_1 (Rlt 1 (maxfg x)) 1 (maxfg x) H1lt).
rewrite the current goal using Heq (from left to right) at position 1.
An exact proof term for the current goal is (SepI R (λr : set ⇒ order_rel R r b) 1 real_1 (Rlt_implies_order_rel_R 1 b H1ltb)).
Assume Hn1lt: ¬ (Rlt 1 (maxfg x)).
We prove the intermediate claim HmaxR: maxfg x ∈ R.
We prove the intermediate claim Hdef: maxfg x = (if (Rlt (apply_fun f x) (apply_fun g x)) then (apply_fun g x) else (apply_fun f x)).
Use reflexivity.
rewrite the current goal using Hdef (from left to right) at position 1.
Apply (xm (Rlt (apply_fun f x) (apply_fun g x))) to the current goal.
Assume Hfg: Rlt (apply_fun f x) (apply_fun g x).
We prove the intermediate claim Heq: (if (Rlt (apply_fun f x) (apply_fun g x)) then (apply_fun g x) else (apply_fun f x)) = (apply_fun g x).
An exact proof term for the current goal is (If_i_1 (Rlt (apply_fun f x) (apply_fun g x)) (apply_fun g x) (apply_fun f x) Hfg).
rewrite the current goal using Heq (from left to right) at position 1.
An exact proof term for the current goal is (HgFun x HxX).
Assume Hnfg: ¬ (Rlt (apply_fun f x) (apply_fun g x)).
We prove the intermediate claim Heq: (if (Rlt (apply_fun f x) (apply_fun g x)) then (apply_fun g x) else (apply_fun f x)) = (apply_fun f x).
An exact proof term for the current goal is (If_i_0 (Rlt (apply_fun f x) (apply_fun g x)) (apply_fun g x) (apply_fun f x) Hnfg).
rewrite the current goal using Heq (from left to right) at position 1.
An exact proof term for the current goal is (HfFun x HxX).
We prove the intermediate claim Hle: Rle (maxfg x) 1.
An exact proof term for the current goal is (RleI (maxfg x) 1 HmaxR real_1 Hn1lt).
We prove the intermediate claim Hlt: Rlt (maxfg x) b.
An exact proof term for the current goal is (Rle_Rlt_tra (maxfg x) 1 b Hle H1ltb).
We prove the intermediate claim Heq: (if (Rlt 1 (maxfg x)) then 1 else (maxfg x)) = (maxfg x).
An exact proof term for the current goal is (If_i_0 (Rlt 1 (maxfg x)) 1 (maxfg x) Hn1lt).
rewrite the current goal using Heq (from left to right) at position 1.
An exact proof term for the current goal is (SepI R (λr : set ⇒ order_rel R r b) (maxfg x) HmaxR (Rlt_implies_order_rel_R (maxfg x) b Hlt)).
An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun h u ∈ open_ray_lower R b) x HxX HhxRay).
rewrite the current goal using HpreEq (from left to right).
An exact proof term for the current goal is (topology_has_X X Tx HTx).
Assume Hn1ltb: ¬ (Rlt 1 b).
We prove the intermediate claim HbLe1: Rle b 1.
An exact proof term for the current goal is (RleI b 1 HbR real_1 Hn1ltb).
We prove the intermediate claim HpreEq: preimage_of X h (open_ray_lower R b) = Lf ∩ Lg.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ preimage_of X h (open_ray_lower R b).
We will prove x ∈ Lf ∩ Lg.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λu : set ⇒ apply_fun h u ∈ open_ray_lower R b) x Hx).
We prove the intermediate claim HhxRay: apply_fun h x ∈ open_ray_lower R b.
An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun h u ∈ open_ray_lower R b) x Hx).
We prove the intermediate claim Hrel: order_rel R (apply_fun h x) b.
An exact proof term for the current goal is (SepE2 R (λr : set ⇒ order_rel R r b) (apply_fun h x) HhxRay).
We prove the intermediate claim Hlt: Rlt (apply_fun h x) b.
An exact proof term for the current goal is (order_rel_R_implies_Rlt (apply_fun h x) b Hrel).
We prove the intermediate claim HhxEq: apply_fun h x = h0 x.
An exact proof term for the current goal is (apply_fun_graph X (λu : set ⇒ h0 u) x HxX).
We prove the intermediate claim Hlt0: Rlt (h0 x) b.
rewrite the current goal using HhxEq (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
We prove the intermediate claim Hdef0: h0 x = (if (Rlt 1 (maxfg x)) then 1 else (maxfg x)).
Use reflexivity.
We prove the intermediate claim Hn1lt: ¬ (Rlt 1 (maxfg x)).
Assume H1lt: Rlt 1 (maxfg x).
We prove the intermediate claim HeqIf: (if (Rlt 1 (maxfg x)) then 1 else (maxfg x)) = 1.
An exact proof term for the current goal is (If_i_1 (Rlt 1 (maxfg x)) 1 (maxfg x) H1lt).
We prove the intermediate claim Heq: h0 x = 1.
rewrite the current goal using Hdef0 (from left to right) at position 1.
An exact proof term for the current goal is HeqIf.
We prove the intermediate claim H1ltb: Rlt 1 b.
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is Hlt0.
An exact proof term for the current goal is (Hn1ltb H1ltb).
We prove the intermediate claim HeqIf: (if (Rlt 1 (maxfg x)) then 1 else (maxfg x)) = (maxfg x).
An exact proof term for the current goal is (If_i_0 (Rlt 1 (maxfg x)) 1 (maxfg x) Hn1lt).
We prove the intermediate claim Heq: h0 x = maxfg x.
rewrite the current goal using Hdef0 (from left to right) at position 1.
An exact proof term for the current goal is HeqIf.
We prove the intermediate claim Hmaxlt: Rlt (maxfg x) b.
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is Hlt0.
We prove the intermediate claim Hfb: Rlt (apply_fun f x) b.
Apply (xm (Rlt (apply_fun f x) (apply_fun g x))) to the current goal.
Assume Hfg: Rlt (apply_fun f x) (apply_fun g x).
We prove the intermediate claim HeqM: maxfg x = apply_fun g x.
An exact proof term for the current goal is (If_i_1 (Rlt (apply_fun f x) (apply_fun g x)) (apply_fun g x) (apply_fun f x) Hfg).
We prove the intermediate claim HgbLt: Rlt (apply_fun g x) b.
rewrite the current goal using HeqM (from right to left) at position 1.
An exact proof term for the current goal is Hmaxlt.
An exact proof term for the current goal is (Rlt_tra (apply_fun f x) (apply_fun g x) b Hfg HgbLt).
Assume Hnfg: ¬ (Rlt (apply_fun f x) (apply_fun g x)).
We prove the intermediate claim HeqM: maxfg x = apply_fun f x.
An exact proof term for the current goal is (If_i_0 (Rlt (apply_fun f x) (apply_fun g x)) (apply_fun g x) (apply_fun f x) Hnfg).
We prove the intermediate claim HfbLt: Rlt (apply_fun f x) b.
rewrite the current goal using HeqM (from right to left) at position 1.
An exact proof term for the current goal is Hmaxlt.
An exact proof term for the current goal is HfbLt.
We prove the intermediate claim Hgb: Rlt (apply_fun g x) b.
Apply (xm (Rlt (apply_fun f x) (apply_fun g x))) to the current goal.
Assume Hfg: Rlt (apply_fun f x) (apply_fun g x).
We prove the intermediate claim HeqM: maxfg x = apply_fun g x.
An exact proof term for the current goal is (If_i_1 (Rlt (apply_fun f x) (apply_fun g x)) (apply_fun g x) (apply_fun f x) Hfg).
We prove the intermediate claim HgbLt: Rlt (apply_fun g x) b.
rewrite the current goal using HeqM (from right to left) at position 1.
An exact proof term for the current goal is Hmaxlt.
An exact proof term for the current goal is HgbLt.
Assume Hnfg: ¬ (Rlt (apply_fun f x) (apply_fun g x)).
We prove the intermediate claim HeqM: maxfg x = apply_fun f x.
An exact proof term for the current goal is (If_i_0 (Rlt (apply_fun f x) (apply_fun g x)) (apply_fun g x) (apply_fun f x) Hnfg).
We prove the intermediate claim HfbLt: Rlt (apply_fun f x) b.
rewrite the current goal using HeqM (from right to left) at position 1.
An exact proof term for the current goal is Hmaxlt.
We prove the intermediate claim HgxR: apply_fun g x ∈ R.
An exact proof term for the current goal is (HgFun x HxX).
We prove the intermediate claim HfxR: apply_fun f x ∈ R.
An exact proof term for the current goal is (HfFun x HxX).
We prove the intermediate claim Hle: Rle (apply_fun g x) (apply_fun f x).
An exact proof term for the current goal is (RleI (apply_fun g x) (apply_fun f x) HgxR HfxR Hnfg).
An exact proof term for the current goal is (Rle_Rlt_tra (apply_fun g x) (apply_fun f x) b Hle HfbLt).
We prove the intermediate claim HfxR: apply_fun f x ∈ R.
An exact proof term for the current goal is (HfFun x HxX).
We prove the intermediate claim HgxR: apply_fun g x ∈ R.
An exact proof term for the current goal is (HgFun x HxX).
We prove the intermediate claim HfxRay: apply_fun f x ∈ open_ray_lower R b.
An exact proof term for the current goal is (SepI R (λr : set ⇒ order_rel R r b) (apply_fun f x) HfxR (Rlt_implies_order_rel_R (apply_fun f x) b Hfb)).
We prove the intermediate claim HgxRay: apply_fun g x ∈ open_ray_lower R b.
An exact proof term for the current goal is (SepI R (λr : set ⇒ order_rel R r b) (apply_fun g x) HgxR (Rlt_implies_order_rel_R (apply_fun g x) b Hgb)).
We prove the intermediate claim HxLf: x ∈ Lf.
An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun f u ∈ open_ray_lower R b) x HxX HfxRay).
We prove the intermediate claim HxLg: x ∈ Lg.
An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun g u ∈ open_ray_lower R b) x HxX HgxRay).
An exact proof term for the current goal is (binintersectI Lf Lg x HxLf HxLg).
Let x be given.
Assume Hx: x ∈ Lf ∩ Lg.
We will prove x ∈ preimage_of X h (open_ray_lower R b).
We prove the intermediate claim HxLf: x ∈ Lf.
An exact proof term for the current goal is (binintersectE1 Lf Lg x Hx).
We prove the intermediate claim HxLg: x ∈ Lg.
An exact proof term for the current goal is (binintersectE2 Lf Lg x Hx).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λu : set ⇒ apply_fun f u ∈ open_ray_lower R b) x HxLf).
We prove the intermediate claim HfxRay: apply_fun f x ∈ open_ray_lower R b.
An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun f u ∈ open_ray_lower R b) x HxLf).
We prove the intermediate claim HgxRay: apply_fun g x ∈ open_ray_lower R b.
An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun g u ∈ open_ray_lower R b) x HxLg).
We prove the intermediate claim Hfb: Rlt (apply_fun f x) b.
An exact proof term for the current goal is (order_rel_R_implies_Rlt (apply_fun f x) b (SepE2 R (λr : set ⇒ order_rel R r b) (apply_fun f x) HfxRay)).
We prove the intermediate claim Hgb: Rlt (apply_fun g x) b.
An exact proof term for the current goal is (order_rel_R_implies_Rlt (apply_fun g x) b (SepE2 R (λr : set ⇒ order_rel R r b) (apply_fun g x) HgxRay)).
We prove the intermediate claim Hmaxlt: Rlt (maxfg x) b.
Apply (xm (Rlt (apply_fun f x) (apply_fun g x))) to the current goal.
Assume Hfg: Rlt (apply_fun f x) (apply_fun g x).
We prove the intermediate claim HeqM: maxfg x = apply_fun g x.
An exact proof term for the current goal is (If_i_1 (Rlt (apply_fun f x) (apply_fun g x)) (apply_fun g x) (apply_fun f x) Hfg).
rewrite the current goal using HeqM (from left to right).
An exact proof term for the current goal is Hgb.
Assume Hnfg: ¬ (Rlt (apply_fun f x) (apply_fun g x)).
We prove the intermediate claim HeqM: maxfg x = apply_fun f x.
An exact proof term for the current goal is (If_i_0 (Rlt (apply_fun f x) (apply_fun g x)) (apply_fun g x) (apply_fun f x) Hnfg).
rewrite the current goal using HeqM (from left to right).
An exact proof term for the current goal is Hfb.
We prove the intermediate claim HmaxR: maxfg x ∈ R.
We prove the intermediate claim Hdef: maxfg x = (if (Rlt (apply_fun f x) (apply_fun g x)) then (apply_fun g x) else (apply_fun f x)).
Use reflexivity.
rewrite the current goal using Hdef (from left to right) at position 1.
Apply (xm (Rlt (apply_fun f x) (apply_fun g x))) to the current goal.
Assume Hfg: Rlt (apply_fun f x) (apply_fun g x).
We prove the intermediate claim Heq: (if (Rlt (apply_fun f x) (apply_fun g x)) then (apply_fun g x) else (apply_fun f x)) = (apply_fun g x).
An exact proof term for the current goal is (If_i_1 (Rlt (apply_fun f x) (apply_fun g x)) (apply_fun g x) (apply_fun f x) Hfg).
rewrite the current goal using Heq (from left to right) at position 1.
An exact proof term for the current goal is (HgFun x HxX).
Assume Hnfg: ¬ (Rlt (apply_fun f x) (apply_fun g x)).
We prove the intermediate claim Heq: (if (Rlt (apply_fun f x) (apply_fun g x)) then (apply_fun g x) else (apply_fun f x)) = (apply_fun f x).
An exact proof term for the current goal is (If_i_0 (Rlt (apply_fun f x) (apply_fun g x)) (apply_fun g x) (apply_fun f x) Hnfg).
rewrite the current goal using Heq (from left to right) at position 1.
An exact proof term for the current goal is (HfFun x HxX).
We prove the intermediate claim HmaxLe1: Rle (maxfg x) 1.
We prove the intermediate claim HmaxLt1: Rlt (maxfg x) 1.
An exact proof term for the current goal is (Rlt_Rle_tra (maxfg x) b 1 Hmaxlt HbLe1).
An exact proof term for the current goal is (Rlt_implies_Rle (maxfg x) 1 HmaxLt1).
We prove the intermediate claim Hn1lt: ¬ (Rlt 1 (maxfg x)).
Assume H1lt: Rlt 1 (maxfg x).
An exact proof term for the current goal is ((RleE_nlt (maxfg x) 1 HmaxLe1) H1lt).
We prove the intermediate claim Heq0: h0 x = maxfg x.
An exact proof term for the current goal is (If_i_0 (Rlt 1 (maxfg x)) 1 (maxfg x) Hn1lt).
We prove the intermediate claim HhxRay: apply_fun h x ∈ open_ray_lower R b.
We prove the intermediate claim HhxEq: apply_fun h x = h0 x.
An exact proof term for the current goal is (apply_fun_graph X (λu : set ⇒ h0 u) x HxX).
rewrite the current goal using HhxEq (from left to right).
rewrite the current goal using Heq0 (from left to right) at position 1.
An exact proof term for the current goal is (SepI R (λr : set ⇒ order_rel R r b) (maxfg x) HmaxR (Rlt_implies_order_rel_R (maxfg x) b Hmaxlt)).
An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun h u ∈ open_ray_lower R b) x HxX HhxRay).
rewrite the current goal using HpreEq (from left to right).
An exact proof term for the current goal is (topology_binintersect_closed X Tx Lf Lg HTx HLf HLg).
An exact proof term for the current goal is Hs0.
Assume HsR: s ∈ {R}.
We prove the intermediate claim Hseq: s = R.
An exact proof term for the current goal is (SingE R s HsR).
rewrite the current goal using Hseq (from left to right).
We prove the intermediate claim HpreEq: preimage_of X h R = X.
An exact proof term for the current goal is (preimage_of_whole X R h Hfunh).
rewrite the current goal using HpreEq (from left to right) at position 1.
An exact proof term for the current goal is (topology_has_X X Tx HTx).
An exact proof term for the current goal is HsS.
We prove the intermediate claim Hhx0: apply_fun h x0 = h0 x0.
An exact proof term for the current goal is (apply_fun_graph X (λu : set ⇒ h0 u) x0 Hx0X).
rewrite the current goal using Hhx0 (from left to right).
We prove the intermediate claim Hmax0: maxfg x0 = 0.
We prove the intermediate claim HdefM: maxfg x0 = (if (Rlt (apply_fun f x0) (apply_fun g x0)) then (apply_fun g x0) else (apply_fun f x0)).
Use reflexivity.
rewrite the current goal using HdefM (from left to right).
rewrite the current goal using Hfx0 (from left to right).
rewrite the current goal using Hgx0 (from left to right).
We prove the intermediate claim Hnlt00: ¬ (Rlt 0 0).
An exact proof term for the current goal is (not_Rlt_refl 0 real_0).
rewrite the current goal using (If_i_0 (Rlt 0 0) 0 0 Hnlt00) (from left to right).
Use reflexivity.
We prove the intermediate claim Hdef0: h0 x0 = (if (Rlt 1 (maxfg x0)) then 1 else (maxfg x0)).
Use reflexivity.
rewrite the current goal using Hdef0 (from left to right).
rewrite the current goal using Hmax0 (from left to right).
We prove the intermediate claim Hnlt10: ¬ (Rlt 1 0).
An exact proof term for the current goal is (not_Rlt_sym 0 1 Rlt_0_1).
rewrite the current goal using (If_i_0 (Rlt 1 0) 1 0 Hnlt10) (from left to right).
Use reflexivity.
Let y be given.
Assume HyX: y ∈ X.
Assume Hor: apply_fun f y = 1 ∨ apply_fun g y = 1.
We will prove (apply_fun h y = 1).
We prove the intermediate claim Hhy: apply_fun h y = h0 y.
An exact proof term for the current goal is (apply_fun_graph X (λu : set ⇒ h0 u) y HyX).
rewrite the current goal using Hhy (from left to right).
We prove the intermediate claim Hdef0y: h0 y = (if (Rlt 1 (maxfg y)) then 1 else (maxfg y)).
Use reflexivity.
rewrite the current goal using Hdef0y (from left to right).
Apply (xm (Rlt 1 (maxfg y))) to the current goal.
Assume H1ltMax: Rlt 1 (maxfg y).
We prove the intermediate claim Heq: (if (Rlt 1 (maxfg y)) then 1 else (maxfg y)) = 1.
An exact proof term for the current goal is (If_i_1 (Rlt 1 (maxfg y)) 1 (maxfg y) H1ltMax).
rewrite the current goal using Heq (from left to right) at position 1.
Use reflexivity.
Assume Hn1ltMax: ¬ (Rlt 1 (maxfg y)).
We prove the intermediate claim Heq: (if (Rlt 1 (maxfg y)) then 1 else (maxfg y)) = (maxfg y).
An exact proof term for the current goal is (If_i_0 (Rlt 1 (maxfg y)) 1 (maxfg y) Hn1ltMax).
rewrite the current goal using Heq (from left to right) at position 1.
Apply Hor to the current goal.
Assume Hfy1: apply_fun f y = 1.
We prove the intermediate claim HdefM: maxfg y = (if (Rlt (apply_fun f y) (apply_fun g y)) then (apply_fun g y) else (apply_fun f y)).
Use reflexivity.
rewrite the current goal using HdefM (from left to right).
Apply (xm (Rlt (apply_fun f y) (apply_fun g y))) to the current goal.
Assume Hfg: Rlt (apply_fun f y) (apply_fun g y).
We prove the intermediate claim HeqIf: (if (Rlt (apply_fun f y) (apply_fun g y)) then (apply_fun g y) else (apply_fun f y)) = (apply_fun g y).
An exact proof term for the current goal is (If_i_1 (Rlt (apply_fun f y) (apply_fun g y)) (apply_fun g y) (apply_fun f y) Hfg).
rewrite the current goal using HeqIf (from left to right) at position 1.
We prove the intermediate claim H1ltg: Rlt 1 (apply_fun g y).
rewrite the current goal using Hfy1 (from right to left) at position 1.
An exact proof term for the current goal is Hfg.
We prove the intermediate claim HmaxEq: maxfg y = apply_fun g y.
rewrite the current goal using HdefM (from left to right) at position 1.
An exact proof term for the current goal is (If_i_1 (Rlt (apply_fun f y) (apply_fun g y)) (apply_fun g y) (apply_fun f y) Hfg).
We prove the intermediate claim H1ltMax': Rlt 1 (maxfg y).
rewrite the current goal using HmaxEq (from left to right).
An exact proof term for the current goal is H1ltg.
An exact proof term for the current goal is (FalseE (Hn1ltMax H1ltMax') (apply_fun g y = 1)).
Assume Hnfg: ¬ (Rlt (apply_fun f y) (apply_fun g y)).
We prove the intermediate claim HeqIf: (if (Rlt (apply_fun f y) (apply_fun g y)) then (apply_fun g y) else (apply_fun f y)) = (apply_fun f y).
An exact proof term for the current goal is (If_i_0 (Rlt (apply_fun f y) (apply_fun g y)) (apply_fun g y) (apply_fun f y) Hnfg).
rewrite the current goal using HeqIf (from left to right) at position 1.
rewrite the current goal using Hfy1 (from left to right).
Use reflexivity.
Assume Hgy1: apply_fun g y = 1.
We prove the intermediate claim HdefM: maxfg y = (if (Rlt (apply_fun f y) (apply_fun g y)) then (apply_fun g y) else (apply_fun f y)).
Use reflexivity.
rewrite the current goal using HdefM (from left to right).
Apply (xm (Rlt (apply_fun f y) (apply_fun g y))) to the current goal.
Assume Hfg: Rlt (apply_fun f y) (apply_fun g y).
We prove the intermediate claim HeqIf: (if (Rlt (apply_fun f y) (apply_fun g y)) then (apply_fun g y) else (apply_fun f y)) = (apply_fun g y).
An exact proof term for the current goal is (If_i_1 (Rlt (apply_fun f y) (apply_fun g y)) (apply_fun g y) (apply_fun f y) Hfg).
rewrite the current goal using HeqIf (from left to right) at position 1.
rewrite the current goal using Hgy1 (from left to right).
Use reflexivity.
Assume Hnfg: ¬ (Rlt (apply_fun f y) (apply_fun g y)).
We prove the intermediate claim HeqIf: (if (Rlt (apply_fun f y) (apply_fun g y)) then (apply_fun g y) else (apply_fun f y)) = (apply_fun f y).
An exact proof term for the current goal is (If_i_0 (Rlt (apply_fun f y) (apply_fun g y)) (apply_fun g y) (apply_fun f y) Hnfg).
rewrite the current goal using HeqIf (from left to right) at position 1.
We prove the intermediate claim HfyR: apply_fun f y ∈ R.
An exact proof term for the current goal is (HfFun y HyX).
We prove the intermediate claim HgyR: apply_fun g y ∈ R.
An exact proof term for the current goal is (HgFun y HyX).
We prove the intermediate claim Hlegf: Rle (apply_fun g y) (apply_fun f y).
An exact proof term for the current goal is (RleI (apply_fun g y) (apply_fun f y) HgyR HfyR Hnfg).
We prove the intermediate claim Hle1f: Rle 1 (apply_fun f y).
rewrite the current goal using Hgy1 (from right to left) at position 1.
An exact proof term for the current goal is Hlegf.
We prove the intermediate claim HmaxEq: maxfg y = apply_fun f y.
rewrite the current goal using HdefM (from left to right) at position 1.
An exact proof term for the current goal is (If_i_0 (Rlt (apply_fun f y) (apply_fun g y)) (apply_fun g y) (apply_fun f y) Hnfg).
We prove the intermediate claim Hn1ltf: ¬ (Rlt 1 (apply_fun f y)).
Assume H1ltf: Rlt 1 (apply_fun f y).
We prove the intermediate claim H1ltMax': Rlt 1 (maxfg y).
rewrite the current goal using HmaxEq (from left to right).
An exact proof term for the current goal is H1ltf.
An exact proof term for the current goal is (Hn1ltMax H1ltMax').
We prove the intermediate claim Hlef1: Rle (apply_fun f y) 1.
An exact proof term for the current goal is (RleI (apply_fun f y) 1 HfyR real_1 Hn1ltf).
We prove the intermediate claim Heqfy1: apply_fun f y = 1.
An exact proof term for the current goal is (Rle_antisym (apply_fun f y) 1 Hlef1 Hle1f).
rewrite the current goal using Heqfy1 (from left to right).
Use reflexivity.
∎