Let a be given.
Assume HaR: a ∈ R.
Assume Hanlt0: ¬ (Rlt a 0).
Assume Halt1: Rlt a 1.
We will prove preimage_of R normalize01_fun (open_ray_upper R a) ∈ R_standard_topology.
Apply xm (Rlt 0 a) to the current goal.
Assume H0lta: Rlt 0 a.
Set W to be the term preimage_of R normalize01_fun (open_ray_upper R a).
Set Tx to be the term R_standard_topology.
Set id to be the term {(x,x)|x ∈ R}.
Set m1 to be the term const_fun R (minus_SNo 1).
Set numf to be the term compose_fun R (pair_map R id id) mul_fun_R.
Set shift to be the term compose_fun R (pair_map R id m1) add_fun_R.
Set shift2 to be the term compose_fun R (pair_map R shift shift) mul_fun_R.
Set denf to be the term compose_fun R (pair_map R numf shift2) add_fun_R.
Set dena to be the term compose_fun R denf (mul_const_fun a).
Set pair to be the term pair_map R dena numf.
Set Lt to be the term {p ∈ EuclidPlane|Rlt (p 0) (p 1)}.
We prove the intermediate claim HTx: topology_on R Tx.
An exact proof term for the current goal is R_standard_topology_is_topology_local.
We prove the intermediate claim Hid: continuous_map R Tx R Tx id.
An exact proof term for the current goal is (identity_continuous R Tx HTx).
We prove the intermediate claim Hm1R: minus_SNo 1 ∈ R.
An exact proof term for the current goal is (real_minus_SNo 1 real_1).
We prove the intermediate claim Hm1cont: continuous_map R Tx R Tx m1.
An exact proof term for the current goal is (const_fun_continuous R Tx R Tx (minus_SNo 1) HTx HTx Hm1R).
We prove the intermediate claim Hnumcont: continuous_map R Tx R Tx numf.
An exact proof term for the current goal is (mul_two_continuous_R R Tx id id HTx Hid Hid).
We prove the intermediate claim Hshiftcont: continuous_map R Tx R Tx shift.
An exact proof term for the current goal is (add_two_continuous_R R Tx id m1 HTx Hid Hm1cont).
We prove the intermediate claim Hshift2cont: continuous_map R Tx R Tx shift2.
An exact proof term for the current goal is (mul_two_continuous_R R Tx shift shift HTx Hshiftcont Hshiftcont).
We prove the intermediate claim Hdencont: continuous_map R Tx R Tx denf.
An exact proof term for the current goal is (add_two_continuous_R R Tx numf shift2 HTx Hnumcont Hshift2cont).
We prove the intermediate claim Hmulconst: continuous_map R Tx R Tx (mul_const_fun a).
An exact proof term for the current goal is (mul_const_fun_continuous a HaR).
We prove the intermediate claim Hdenc: continuous_map R Tx R Tx dena.
An exact proof term for the current goal is (composition_continuous R Tx R Tx R Tx denf (mul_const_fun a) Hdencont Hmulconst).
We prove the intermediate claim Hpaircont: continuous_map R Tx EuclidPlane R2_standard_topology pair.
An exact proof term for the current goal is (maps_into_products_axiom R Tx R Tx R Tx dena numf Hdenc Hnumcont).
We prove the intermediate claim HLtopen: Lt ∈ R2_standard_topology.
An exact proof term for the current goal is R2_strict_lt_open.
We prove the intermediate claim HWeq: W = preimage_of R pair Lt.
Apply set_ext to the current goal.
Let t be given.
Assume HtW: t ∈ W.
We will prove t ∈ preimage_of R pair Lt.
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ apply_fun normalize01_fun x0 ∈ open_ray_upper R a) t HtW).
We prove the intermediate claim HtRay: apply_fun normalize01_fun t ∈ open_ray_upper R a.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ apply_fun normalize01_fun x0 ∈ open_ray_upper R a) t HtW).
We prove the intermediate claim Hiff: (apply_fun normalize01_fun t ∈ open_ray_upper R a ↔ Rlt a (apply_fun normalize01_fun t)).
An exact proof term for the current goal is (normalize01_fun_img_in_open_ray_upper_iff a t HaR HtR).
We prove the intermediate claim Halt: Rlt a (apply_fun normalize01_fun t).
An exact proof term for the current goal is (iffEL (apply_fun normalize01_fun t ∈ open_ray_upper R a) (Rlt a (apply_fun normalize01_fun t)) Hiff HtRay).
We prove the intermediate claim HaPos: 0 < a.
An exact proof term for the current goal is (RltE_lt 0 a H0lta).
We prove the intermediate claim HaLt1: a < 1.
An exact proof term for the current goal is (RltE_lt a 1 Halt1).
We prove the intermediate claim HaltS: a < apply_fun normalize01_fun t.
An exact proof term for the current goal is (RltE_lt a (apply_fun normalize01_fun t) Halt).
We prove the intermediate claim HmulIneq: mul_SNo a (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) < (mul_SNo t t).
An exact proof term for the current goal is (iffEL (a < apply_fun normalize01_fun t) (mul_SNo a (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) < (mul_SNo t t)) (normalize01_fun_gt_iff_mul_den_lt_num a t HaR HtR HaPos HaLt1) HaltS).
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 HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim HnumR: mul_SNo t t ∈ R.
An exact proof term for the current goal is (real_mul_SNo t HtR t HtR).
We prove the intermediate claim Hm1R2: minus_SNo 1 ∈ R.
An exact proof term for the current goal is Hm1R.
We prove the intermediate claim HuR: add_SNo t (minus_SNo 1) ∈ R.
An exact proof term for the current goal is (real_add_SNo t HtR (minus_SNo 1) Hm1R2).
We prove the intermediate claim Hu2R: mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)) ∈ R.
An exact proof term for the current goal is (real_mul_SNo (add_SNo t (minus_SNo 1)) HuR (add_SNo t (minus_SNo 1)) HuR).
We prove the intermediate claim HdenR: add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1))) ∈ R.
An exact proof term for the current goal is (real_add_SNo (mul_SNo t t) HnumR (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1))) Hu2R).
We prove the intermediate claim HdenS: SNo (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))).
An exact proof term for the current goal is (real_SNo (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) HdenR).
We prove the intermediate claim Hmulcom: mul_SNo a (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) = mul_SNo (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) a.
An exact proof term for the current goal is (mul_SNo_com a (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) HaS HdenS).
We prove the intermediate claim HmulIneq2: mul_SNo (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) a < (mul_SNo t t).
rewrite the current goal using Hmulcom (from right to left) at position 1.
An exact proof term for the current goal is HmulIneq.
We prove the intermediate claim HdenaR: mul_SNo (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) a ∈ R.
An exact proof term for the current goal is (real_mul_SNo (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) HdenR a HaR).
We prove the intermediate claim HdenaLt: Rlt (mul_SNo (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) a) (mul_SNo t t).
An exact proof term for the current goal is (RltI (mul_SNo (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) a) (mul_SNo t t) HdenaR HnumR HmulIneq2).
We prove the intermediate claim HpairLt: apply_fun pair t ∈ Lt.
We prove the intermediate claim Happ: apply_fun pair t = (apply_fun dena t,apply_fun numf t).
An exact proof term for the current goal is (pair_map_apply R R R dena numf t HtR).
rewrite the current goal using Happ (from left to right).
Apply (SepI EuclidPlane (λp : set ⇒ Rlt (p 0) (p 1)) (apply_fun dena t,apply_fun numf t)) to the current goal.
We prove the intermediate claim Hdena_fun: function_on dena R R.
An exact proof term for the current goal is (continuous_map_function_on R Tx R Tx dena Hdenc).
We prove the intermediate claim Hnumf_fun: function_on numf R R.
An exact proof term for the current goal is (continuous_map_function_on R Tx R Tx numf Hnumcont).
We prove the intermediate claim HdenaR2: apply_fun dena t ∈ R.
An exact proof term for the current goal is (Hdena_fun t HtR).
We prove the intermediate claim HnumfR2: apply_fun numf t ∈ R.
An exact proof term for the current goal is (Hnumf_fun t HtR).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R (apply_fun dena t) (apply_fun numf t) HdenaR2 HnumfR2).
We prove the intermediate claim H0: (apply_fun dena t,apply_fun numf t) 0 = apply_fun dena t.
An exact proof term for the current goal is (tuple_2_0_eq (apply_fun dena t) (apply_fun numf t)).
We prove the intermediate claim H1: (apply_fun dena t,apply_fun numf t) 1 = apply_fun numf t.
An exact proof term for the current goal is (tuple_2_1_eq (apply_fun dena t) (apply_fun numf t)).
rewrite the current goal using H0 (from left to right).
rewrite the current goal using H1 (from left to right).
We prove the intermediate claim HdenaApp: apply_fun dena t = mul_SNo (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) a.
rewrite the current goal using (compose_fun_apply R denf (mul_const_fun a) t HtR) (from left to right).
We prove the intermediate claim Hdenf_fun0: function_on denf R R.
An exact proof term for the current goal is (continuous_map_function_on R Tx R Tx denf Hdencont).
We prove the intermediate claim HdenfR0: apply_fun denf t ∈ R.
An exact proof term for the current goal is (Hdenf_fun0 t HtR).
rewrite the current goal using (mul_const_fun_apply a (apply_fun denf t) HaR HdenfR0) (from left to right).
We prove the intermediate claim HdenfApp: apply_fun denf t = add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1))).
We prove the intermediate claim Hid_fun0: function_on id R R.
An exact proof term for the current goal is (continuous_map_function_on R Tx R Tx id Hid).
We prove the intermediate claim Hm1_fun0: function_on m1 R R.
An exact proof term for the current goal is (continuous_map_function_on R Tx R Tx m1 Hm1cont).
We prove the intermediate claim Hnumf_fun0: function_on numf R R.
An exact proof term for the current goal is (continuous_map_function_on R Tx R Tx numf Hnumcont).
We prove the intermediate claim Hshift_fun0: function_on shift R R.
An exact proof term for the current goal is (continuous_map_function_on R Tx R Tx shift Hshiftcont).
We prove the intermediate claim Hshift2_fun0: function_on shift2 R R.
An exact proof term for the current goal is (continuous_map_function_on R Tx R Tx shift2 Hshift2cont).
We prove the intermediate claim HidR0: apply_fun id t ∈ R.
An exact proof term for the current goal is (Hid_fun0 t HtR).
We prove the intermediate claim Hm1R0: apply_fun m1 t ∈ R.
An exact proof term for the current goal is (Hm1_fun0 t HtR).
We prove the intermediate claim HnumfR0: apply_fun numf t ∈ R.
An exact proof term for the current goal is (Hnumf_fun0 t HtR).
We prove the intermediate claim HshiftR0: apply_fun shift t ∈ R.
An exact proof term for the current goal is (Hshift_fun0 t HtR).
We prove the intermediate claim Hshift2R0: apply_fun shift2 t ∈ R.
An exact proof term for the current goal is (Hshift2_fun0 t HtR).
We prove the intermediate claim HshiftApp: apply_fun shift t = add_SNo t (minus_SNo 1).
rewrite the current goal using (add_of_pair_map_apply R id m1 t HtR HidR0 Hm1R0) (from left to right).
rewrite the current goal using (identity_function_apply R t HtR) (from left to right) at position 1.
rewrite the current goal using (const_fun_apply R (minus_SNo 1) t HtR) (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim HnumApp: apply_fun numf t = mul_SNo t t.
rewrite the current goal using (mul_of_pair_map_apply R id id t HtR HidR0 HidR0) (from left to right).
rewrite the current goal using (identity_function_apply R t HtR) (from left to right) at position 1.
rewrite the current goal using (identity_function_apply R t HtR) (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim Hshift2App: apply_fun shift2 t = mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)).
rewrite the current goal using (mul_of_pair_map_apply R shift shift t HtR HshiftR0 HshiftR0) (from left to right).
rewrite the current goal using HshiftApp (from left to right) at position 1.
rewrite the current goal using HshiftApp (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using (add_of_pair_map_apply R numf shift2 t HtR HnumfR0 Hshift2R0) (from left to right).
rewrite the current goal using HnumApp (from left to right) at position 1.
rewrite the current goal using Hshift2App (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using HdenfApp (from left to right).
Use reflexivity.
rewrite the current goal using HdenaApp (from left to right).
We prove the intermediate claim HnumApp2: apply_fun numf t = mul_SNo t t.
We prove the intermediate claim Hid_fun2: function_on id R R.
An exact proof term for the current goal is (continuous_map_function_on R Tx R Tx id Hid).
We prove the intermediate claim HidR2: apply_fun id t ∈ R.
An exact proof term for the current goal is (Hid_fun2 t HtR).
rewrite the current goal using (mul_of_pair_map_apply R id id t HtR HidR2 HidR2) (from left to right).
rewrite the current goal using (identity_function_apply R t HtR) (from left to right) at position 1.
rewrite the current goal using (identity_function_apply R t HtR) (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using HnumApp2 (from left to right).
An exact proof term for the current goal is HdenaLt.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ apply_fun pair x0 ∈ Lt) t HtR HpairLt).
Let t be given.
Assume HtPre: t ∈ preimage_of R pair Lt.
We will prove t ∈ W.
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ apply_fun pair x0 ∈ Lt) t HtPre).
We prove the intermediate claim HtLt: apply_fun pair t ∈ Lt.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ apply_fun pair x0 ∈ Lt) t HtPre).
We prove the intermediate claim Happ: apply_fun pair t = (apply_fun dena t,apply_fun numf t).
An exact proof term for the current goal is (pair_map_apply R R R dena numf t HtR).
We prove the intermediate claim Hlt: Rlt (apply_fun dena t) (apply_fun numf t).
We prove the intermediate claim Hlt0: Rlt ((apply_fun pair t) 0) ((apply_fun pair t) 1).
An exact proof term for the current goal is (SepE2 EuclidPlane (λp : set ⇒ Rlt (p 0) (p 1)) (apply_fun pair t) HtLt).
We prove the intermediate claim H0: (apply_fun pair t) 0 = apply_fun dena t.
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq (apply_fun dena t) (apply_fun numf t)).
We prove the intermediate claim H1: (apply_fun pair t) 1 = apply_fun numf t.
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq (apply_fun dena t) (apply_fun numf t)).
rewrite the current goal using H0 (from right to left).
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hlt0.
We prove the intermediate claim HaPos: 0 < a.
An exact proof term for the current goal is (RltE_lt 0 a H0lta).
We prove the intermediate claim HaLt1: a < 1.
An exact proof term for the current goal is (RltE_lt a 1 Halt1).
We prove the intermediate claim HdenaLtS: apply_fun dena t < apply_fun numf t.
An exact proof term for the current goal is (RltE_lt (apply_fun dena t) (apply_fun numf t) Hlt).
We prove the intermediate claim HnumApp: apply_fun numf t = mul_SNo t t.
We prove the intermediate claim Hid_fun3: function_on id R R.
An exact proof term for the current goal is (continuous_map_function_on R Tx R Tx id Hid).
We prove the intermediate claim HidR3: apply_fun id t ∈ R.
An exact proof term for the current goal is (Hid_fun3 t HtR).
rewrite the current goal using (mul_of_pair_map_apply R id id t HtR HidR3 HidR3) (from left to right).
rewrite the current goal using (identity_function_apply R t HtR) (from left to right) at position 1.
rewrite the current goal using (identity_function_apply R t HtR) (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim HdenaApp: apply_fun dena t = mul_SNo (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) a.
rewrite the current goal using (compose_fun_apply R denf (mul_const_fun a) t HtR) (from left to right).
We prove the intermediate claim Hdenf_fun4: function_on denf R R.
An exact proof term for the current goal is (continuous_map_function_on R Tx R Tx denf Hdencont).
We prove the intermediate claim HdenfR4: apply_fun denf t ∈ R.
An exact proof term for the current goal is (Hdenf_fun4 t HtR).
rewrite the current goal using (mul_const_fun_apply a (apply_fun denf t) HaR HdenfR4) (from left to right).
We prove the intermediate claim HdenfApp: apply_fun denf t = add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1))).
We prove the intermediate claim Hid_fun4: function_on id R R.
An exact proof term for the current goal is (continuous_map_function_on R Tx R Tx id Hid).
We prove the intermediate claim Hm1_fun4: function_on m1 R R.
An exact proof term for the current goal is (continuous_map_function_on R Tx R Tx m1 Hm1cont).
We prove the intermediate claim Hnumf_fun4: function_on numf R R.
An exact proof term for the current goal is (continuous_map_function_on R Tx R Tx numf Hnumcont).
We prove the intermediate claim Hshift_fun4: function_on shift R R.
An exact proof term for the current goal is (continuous_map_function_on R Tx R Tx shift Hshiftcont).
We prove the intermediate claim Hshift2_fun4: function_on shift2 R R.
An exact proof term for the current goal is (continuous_map_function_on R Tx R Tx shift2 Hshift2cont).
We prove the intermediate claim HidR4: apply_fun id t ∈ R.
An exact proof term for the current goal is (Hid_fun4 t HtR).
We prove the intermediate claim Hm1R4: apply_fun m1 t ∈ R.
An exact proof term for the current goal is (Hm1_fun4 t HtR).
We prove the intermediate claim HnumfR4: apply_fun numf t ∈ R.
An exact proof term for the current goal is (Hnumf_fun4 t HtR).
We prove the intermediate claim HshiftR4: apply_fun shift t ∈ R.
An exact proof term for the current goal is (Hshift_fun4 t HtR).
We prove the intermediate claim Hshift2R4: apply_fun shift2 t ∈ R.
An exact proof term for the current goal is (Hshift2_fun4 t HtR).
We prove the intermediate claim HshiftApp: apply_fun shift t = add_SNo t (minus_SNo 1).
rewrite the current goal using (add_of_pair_map_apply R id m1 t HtR HidR4 Hm1R4) (from left to right).
rewrite the current goal using (identity_function_apply R t HtR) (from left to right) at position 1.
rewrite the current goal using (const_fun_apply R (minus_SNo 1) t HtR) (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim Hshift2App: apply_fun shift2 t = mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)).
rewrite the current goal using (mul_of_pair_map_apply R shift shift t HtR HshiftR4 HshiftR4) (from left to right).
rewrite the current goal using HshiftApp (from left to right) at position 1.
rewrite the current goal using HshiftApp (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using (add_of_pair_map_apply R numf shift2 t HtR HnumfR4 Hshift2R4) (from left to right).
rewrite the current goal using HnumApp (from left to right) at position 1.
rewrite the current goal using Hshift2App (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using HdenfApp (from left to right).
Use reflexivity.
We prove the intermediate claim HdenaLtS0: mul_SNo (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) a < mul_SNo t t.
rewrite the current goal using HdenaApp (from right to left) at position 1.
rewrite the current goal using HnumApp (from right to left) at position 1.
An exact proof term for the current goal is HdenaLtS.
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 HdenR: add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1))) ∈ R.
We prove the intermediate claim HnumR2: mul_SNo t t ∈ R.
An exact proof term for the current goal is (real_mul_SNo t HtR t HtR).
We prove the intermediate claim Hm1R2: minus_SNo 1 ∈ R.
An exact proof term for the current goal is Hm1R.
We prove the intermediate claim HuR: add_SNo t (minus_SNo 1) ∈ R.
An exact proof term for the current goal is (real_add_SNo t HtR (minus_SNo 1) Hm1R2).
We prove the intermediate claim Hu2R: mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)) ∈ R.
An exact proof term for the current goal is (real_mul_SNo (add_SNo t (minus_SNo 1)) HuR (add_SNo t (minus_SNo 1)) HuR).
An exact proof term for the current goal is (real_add_SNo (mul_SNo t t) HnumR2 (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1))) Hu2R).
We prove the intermediate claim HdenS: SNo (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))).
An exact proof term for the current goal is (real_SNo (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) HdenR).
We prove the intermediate claim Hmulcom: mul_SNo a (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) = mul_SNo (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) a.
An exact proof term for the current goal is (mul_SNo_com a (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) HaS HdenS).
We prove the intermediate claim Hmul: mul_SNo a (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) < (mul_SNo t t).
rewrite the current goal using Hmulcom (from left to right) at position 1.
An exact proof term for the current goal is HdenaLtS0.
We prove the intermediate claim HaltS: a < apply_fun normalize01_fun t.
An exact proof term for the current goal is (iffER (a < apply_fun normalize01_fun t) (mul_SNo a (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) < (mul_SNo t t)) (normalize01_fun_gt_iff_mul_den_lt_num a t HaR HtR HaPos HaLt1) Hmul).
We prove the intermediate claim HfR: apply_fun normalize01_fun t ∈ R.
An exact proof term for the current goal is (normalize01_fun_value_in_R t HtR).
We prove the intermediate claim HaltR: Rlt a (apply_fun normalize01_fun t).
An exact proof term for the current goal is (RltI a (apply_fun normalize01_fun t) HaR HfR HaltS).
We prove the intermediate claim Hray: apply_fun normalize01_fun t ∈ open_ray_upper R a.
An exact proof term for the current goal is (iffER (apply_fun normalize01_fun t ∈ open_ray_upper R a) (Rlt a (apply_fun normalize01_fun t)) (normalize01_fun_img_in_open_ray_upper_iff a t HaR HtR) HaltR).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ apply_fun normalize01_fun x0 ∈ open_ray_upper R a) t HtR Hray).
We prove the intermediate claim Hpre: preimage_of R pair Lt ∈ Tx.
An exact proof term for the current goal is (continuous_map_preimage R Tx EuclidPlane R2_standard_topology pair Hpaircont Lt HLtopen).
We prove the intermediate claim HWdef: preimage_of R normalize01_fun (open_ray_upper R a) = W.
Use reflexivity.
rewrite the current goal using HWdef (from left to right).
rewrite the current goal using HWeq (from left to right).
An exact proof term for the current goal is Hpre.
Assume Hnlt0a: ¬ (Rlt 0 a).
We prove the intermediate claim Ha0: a = 0.
An exact proof term for the current goal is (R_eq_of_not_Rlt a 0 HaR real_0 Hanlt0 Hnlt0a).
rewrite the current goal using Ha0 (from left to right).
Set W to be the term preimage_of R normalize01_fun (open_ray_upper R 0).
We prove the intermediate claim HWeq: W = R ∖ {0,0}.
Apply set_ext to the current goal.
Let t be given.
Assume HtW: t ∈ W.
We will prove t ∈ R ∖ {0,0}.
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ apply_fun normalize01_fun x0 ∈ open_ray_upper R 0) t HtW).
We prove the intermediate claim HtRay: apply_fun normalize01_fun t ∈ open_ray_upper R 0.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ apply_fun normalize01_fun x0 ∈ open_ray_upper R 0) t HtW).
We prove the intermediate claim Hiff: (apply_fun normalize01_fun t ∈ open_ray_upper R 0 ↔ Rlt 0 (apply_fun normalize01_fun t)).
An exact proof term for the current goal is (normalize01_fun_img_in_open_ray_upper_iff 0 t real_0 HtR).
We prove the intermediate claim H0ltf: Rlt 0 (apply_fun normalize01_fun t).
An exact proof term for the current goal is (iffEL (apply_fun normalize01_fun t ∈ open_ray_upper R 0) (Rlt 0 (apply_fun normalize01_fun t)) Hiff HtRay).
We prove the intermediate claim HtNot0: t ∉ {0,0}.
Assume Ht0pair: t ∈ {0,0}.
We prove the intermediate claim Ht0: t = 0.
Apply (UPairE t 0 0 Ht0pair (t = 0)) to the current goal.
Assume H0.
An exact proof term for the current goal is H0.
Assume H0.
An exact proof term for the current goal is H0.
We prove the intermediate claim Hf0: apply_fun normalize01_fun t = 0.
rewrite the current goal using Ht0 (from left to right).
An exact proof term for the current goal is normalize01_fun_0.
We prove the intermediate claim Hbad: Rlt 0 0.
rewrite the current goal using Hf0 (from right to left) at position 2.
An exact proof term for the current goal is H0ltf.
An exact proof term for the current goal is ((not_Rlt_refl 0 real_0) Hbad).
An exact proof term for the current goal is (setminusI R {0,0} t HtR HtNot0).
Let t be given.
Assume Ht: t ∈ R ∖ {0,0}.
We will prove t ∈ W.
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (setminusE1 R {0,0} t Ht).
We prove the intermediate claim HtNot0: t ∉ {0,0}.
An exact proof term for the current goal is (setminusE2 R {0,0} t Ht).
We prove the intermediate claim Htne0: t ≠ 0.
Assume Ht0: t = 0.
We prove the intermediate claim Ht0pair: t ∈ {0,0}.
rewrite the current goal using Ht0 (from left to right).
An exact proof term for the current goal is (UPairI1 0 0).
An exact proof term for the current goal is (HtNot0 Ht0pair).
We prove the intermediate claim H0ltf: Rlt 0 (apply_fun normalize01_fun t).
An exact proof term for the current goal is (normalize01_fun_pos_of_neq0 t HtR Htne0).
We prove the intermediate claim Hiff: (apply_fun normalize01_fun t ∈ open_ray_upper R 0 ↔ Rlt 0 (apply_fun normalize01_fun t)).
An exact proof term for the current goal is (normalize01_fun_img_in_open_ray_upper_iff 0 t real_0 HtR).
We prove the intermediate claim Hray: apply_fun normalize01_fun t ∈ open_ray_upper R 0.
An exact proof term for the current goal is (iffER (apply_fun normalize01_fun t ∈ open_ray_upper R 0) (Rlt 0 (apply_fun normalize01_fun t)) Hiff H0ltf).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ apply_fun normalize01_fun x0 ∈ open_ray_upper R 0) t HtR Hray).
We prove the intermediate claim HWdef: preimage_of R normalize01_fun (open_ray_upper R 0) = W.
Use reflexivity.
rewrite the current goal using HWdef (from left to right).
rewrite the current goal using HWeq (from left to right).
An exact proof term for the current goal is (R_minus_singleton_in_R_standard_topology 0 real_0).
∎