Let b be given.
Assume HbR: b ∈ R.
Assume Hnlt1: ¬ (Rlt 1 b).
Assume H0ltb: Rlt 0 b.
We will prove preimage_of R normalize01_fun (open_ray_lower R b) ∈ R_standard_topology.
Apply xm (Rlt b 1) to the current goal.
Assume HbLt1: Rlt b 1.
Set W to be the term preimage_of R normalize01_fun (open_ray_lower R b).
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 denb to be the term compose_fun R denf (mul_const_fun b).
Set pair to be the term pair_map R numf denb.
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 b).
An exact proof term for the current goal is (mul_const_fun_continuous b HbR).
We prove the intermediate claim Hdenbc: continuous_map R Tx R Tx denb.
An exact proof term for the current goal is (composition_continuous R Tx R Tx R Tx denf (mul_const_fun b) 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 numf denb Hnumcont Hdenbc).
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_lower R b) t HtW).
We prove the intermediate claim HtRay: apply_fun normalize01_fun t ∈ open_ray_lower R b.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ apply_fun normalize01_fun x0 ∈ open_ray_lower R b) t HtW).
We prove the intermediate claim Hiff: (apply_fun normalize01_fun t ∈ open_ray_lower R b ↔ Rlt (apply_fun normalize01_fun t) b).
An exact proof term for the current goal is (normalize01_fun_img_in_open_ray_lower_iff b t HbR HtR).
We prove the intermediate claim Hlt: Rlt (apply_fun normalize01_fun t) b.
An exact proof term for the current goal is (iffEL (apply_fun normalize01_fun t ∈ open_ray_lower R b) (Rlt (apply_fun normalize01_fun t) b) Hiff HtRay).
We prove the intermediate claim HbPos: 0 < b.
An exact proof term for the current goal is (RltE_lt 0 b H0ltb).
We prove the intermediate claim HltS: apply_fun normalize01_fun t < b.
An exact proof term for the current goal is (RltE_lt (apply_fun normalize01_fun t) b Hlt).
We prove the intermediate claim Hineq: (mul_SNo t t) < mul_SNo b (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 (iffEL (apply_fun normalize01_fun t < b) ((mul_SNo t t) < mul_SNo b (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1))))) (normalize01_fun_lt_iff_num_lt_mul_den b t HbR HtR HbPos) HltS).
We prove the intermediate claim HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim 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 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) (real_minus_SNo 1 real_1)).
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 b (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)))) b.
An exact proof term for the current goal is (mul_SNo_com b (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) HbS HdenS).
We prove the intermediate claim Hineq2: (mul_SNo t t) < mul_SNo (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) b.
rewrite the current goal using Hmulcom (from right to left).
An exact proof term for the current goal is Hineq.
We prove the intermediate claim HrhsR: mul_SNo (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) b ∈ 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 b HbR).
We prove the intermediate claim HrhsLt: Rlt (mul_SNo t t) (mul_SNo (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) b).
An exact proof term for the current goal is (RltI (mul_SNo t t) (mul_SNo (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) b) HnumR HrhsR Hineq2).
We prove the intermediate claim HpairLt: apply_fun pair t ∈ Lt.
We prove the intermediate claim Happ: apply_fun pair t = (apply_fun numf t,apply_fun denb t).
An exact proof term for the current goal is (pair_map_apply R R R numf denb t HtR).
rewrite the current goal using Happ (from left to right).
Apply (SepI EuclidPlane (λp : set ⇒ Rlt (p 0) (p 1)) (apply_fun numf t,apply_fun denb t)) to the current goal.
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 Hdenb_fun: function_on denb R R.
An exact proof term for the current goal is (continuous_map_function_on R Tx R Tx denb Hdenbc).
We prove the intermediate claim HnumfR2: apply_fun numf t ∈ R.
An exact proof term for the current goal is (Hnumf_fun t HtR).
We prove the intermediate claim HdenbR2: apply_fun denb t ∈ R.
An exact proof term for the current goal is (Hdenb_fun t HtR).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R (apply_fun numf t) (apply_fun denb t) HnumfR2 HdenbR2).
We prove the intermediate claim H0: (apply_fun numf t,apply_fun denb t) 0 = apply_fun numf t.
An exact proof term for the current goal is (tuple_2_0_eq (apply_fun numf t) (apply_fun denb t)).
We prove the intermediate claim H1: (apply_fun numf t,apply_fun denb t) 1 = apply_fun denb t.
An exact proof term for the current goal is (tuple_2_1_eq (apply_fun numf t) (apply_fun denb 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 HnumApp: apply_fun numf t = mul_SNo t t.
We prove the intermediate claim Hid_fun5: 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 HidR5: apply_fun id t ∈ R.
An exact proof term for the current goal is (Hid_fun5 t HtR).
rewrite the current goal using (mul_of_pair_map_apply R id id t HtR HidR5 HidR5) (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 HnumApp (from left to right).
We prove the intermediate claim HdenbApp: apply_fun denb t = mul_SNo (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) b.
rewrite the current goal using (compose_fun_apply R denf (mul_const_fun b) t HtR) (from left to right).
We prove the intermediate claim Hdenf_fun6: 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 HdenfR6: apply_fun denf t ∈ R.
An exact proof term for the current goal is (Hdenf_fun6 t HtR).
rewrite the current goal using (mul_const_fun_apply b (apply_fun denf t) HbR HdenfR6) (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 Hnumf_fun6: 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_fun6: 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_fun6: 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 HnumfR6: apply_fun numf t ∈ R.
An exact proof term for the current goal is (Hnumf_fun6 t HtR).
We prove the intermediate claim HshiftR6: apply_fun shift t ∈ R.
An exact proof term for the current goal is (Hshift_fun6 t HtR).
We prove the intermediate claim Hshift2R6: apply_fun shift2 t ∈ R.
An exact proof term for the current goal is (Hshift2_fun6 t HtR).
We prove the intermediate claim Hid_fun6: 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_fun6: 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 HidR6: apply_fun id t ∈ R.
An exact proof term for the current goal is (Hid_fun6 t HtR).
We prove the intermediate claim Hm1R6: apply_fun m1 t ∈ R.
An exact proof term for the current goal is (Hm1_fun6 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 HidR6 Hm1R6) (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 HshiftR6 HshiftR6) (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 HnumfR6 Hshift2R6) (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 HdenbApp (from left to right).
An exact proof term for the current goal is HrhsLt.
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 HbPos: 0 < b.
An exact proof term for the current goal is (RltE_lt 0 b H0ltb).
We prove the intermediate claim Happ: apply_fun pair t = (apply_fun numf t,apply_fun denb t).
An exact proof term for the current goal is (pair_map_apply R R R numf denb t HtR).
We prove the intermediate claim Hlt: Rlt (apply_fun numf t) (apply_fun denb 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 numf 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 numf t) (apply_fun denb t)).
We prove the intermediate claim H1: (apply_fun pair t) 1 = apply_fun denb 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 numf t) (apply_fun denb 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 HltS: apply_fun numf t < apply_fun denb t.
An exact proof term for the current goal is (RltE_lt (apply_fun numf t) (apply_fun denb t) Hlt).
We prove the intermediate claim HnumApp: apply_fun numf t = mul_SNo t t.
We prove the intermediate claim Hid_fun7: 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 HidR7: apply_fun id t ∈ R.
An exact proof term for the current goal is (Hid_fun7 t HtR).
rewrite the current goal using (mul_of_pair_map_apply R id id t HtR HidR7 HidR7) (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 HdenbApp: apply_fun denb t = mul_SNo (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) b.
rewrite the current goal using (compose_fun_apply R denf (mul_const_fun b) t HtR) (from left to right).
We prove the intermediate claim Hdenf_fun8: 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 HdenfR8: apply_fun denf t ∈ R.
An exact proof term for the current goal is (Hdenf_fun8 t HtR).
rewrite the current goal using (mul_const_fun_apply b (apply_fun denf t) HbR HdenfR8) (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 Hnumf_fun8: 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_fun8: 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_fun8: 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 HnumfR8: apply_fun numf t ∈ R.
An exact proof term for the current goal is (Hnumf_fun8 t HtR).
We prove the intermediate claim HshiftR8: apply_fun shift t ∈ R.
An exact proof term for the current goal is (Hshift_fun8 t HtR).
We prove the intermediate claim Hshift2R8: apply_fun shift2 t ∈ R.
An exact proof term for the current goal is (Hshift2_fun8 t HtR).
We prove the intermediate claim Hid_fun8: 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_fun8: 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 HidR8: apply_fun id t ∈ R.
An exact proof term for the current goal is (Hid_fun8 t HtR).
We prove the intermediate claim Hm1R8: apply_fun m1 t ∈ R.
An exact proof term for the current goal is (Hm1_fun8 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 HidR8 Hm1R8) (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 HshiftR8 HshiftR8) (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 HnumfR8 Hshift2R8) (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 HltS0: mul_SNo t t < mul_SNo (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) b.
rewrite the current goal using HnumApp (from right to left) at position 1.
rewrite the current goal using HdenbApp (from right to left) at position 1.
An exact proof term for the current goal is HltS.
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 HuR2: add_SNo t (minus_SNo 1) ∈ R.
An exact proof term for the current goal is (real_add_SNo t HtR (minus_SNo 1) (real_minus_SNo 1 real_1)).
We prove the intermediate claim Hu2R2: 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)) HuR2 (add_SNo t (minus_SNo 1)) HuR2).
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))) Hu2R2).
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 HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim Hmulcom: mul_SNo b (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)))) b.
An exact proof term for the current goal is (mul_SNo_com b (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) HbS HdenS).
We prove the intermediate claim Hineq: (mul_SNo t t) < mul_SNo b (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))).
rewrite the current goal using Hmulcom (from left to right).
An exact proof term for the current goal is HltS0.
We prove the intermediate claim HltS2: apply_fun normalize01_fun t < b.
An exact proof term for the current goal is (iffER (apply_fun normalize01_fun t < b) ((mul_SNo t t) < mul_SNo b (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1))))) (normalize01_fun_lt_iff_num_lt_mul_den b t HbR HtR HbPos) Hineq).
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 HltR: Rlt (apply_fun normalize01_fun t) b.
An exact proof term for the current goal is (RltI (apply_fun normalize01_fun t) b HfR HbR HltS2).
We prove the intermediate claim Hray: apply_fun normalize01_fun t ∈ open_ray_lower R b.
An exact proof term for the current goal is (iffER (apply_fun normalize01_fun t ∈ open_ray_lower R b) (Rlt (apply_fun normalize01_fun t) b) (normalize01_fun_img_in_open_ray_lower_iff b t HbR HtR) HltR).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ apply_fun normalize01_fun x0 ∈ open_ray_lower R b) 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_lower R b) = 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 Hnltb1: ¬ (Rlt b 1).
We prove the intermediate claim Hb1: b = 1.
An exact proof term for the current goal is (R_eq_of_not_Rlt b 1 HbR real_1 Hnltb1 Hnlt1).
rewrite the current goal using Hb1 (from left to right).
Set W to be the term preimage_of R normalize01_fun (open_ray_lower R 1).
We prove the intermediate claim HWeq: W = R ∖ {1,1}.
Apply set_ext to the current goal.
Let t be given.
Assume HtW: t ∈ W.
We will prove t ∈ R ∖ {1,1}.
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_lower R 1) t HtW).
We prove the intermediate claim HtRay: apply_fun normalize01_fun t ∈ open_ray_lower R 1.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ apply_fun normalize01_fun x0 ∈ open_ray_lower R 1) t HtW).
We prove the intermediate claim Hiff: (apply_fun normalize01_fun t ∈ open_ray_lower R 1 ↔ Rlt (apply_fun normalize01_fun t) 1).
An exact proof term for the current goal is (normalize01_fun_img_in_open_ray_lower_iff 1 t real_1 HtR).
We prove the intermediate claim Hflt1: Rlt (apply_fun normalize01_fun t) 1.
An exact proof term for the current goal is (iffEL (apply_fun normalize01_fun t ∈ open_ray_lower R 1) (Rlt (apply_fun normalize01_fun t) 1) Hiff HtRay).
We prove the intermediate claim HtNot1: t ∉ {1,1}.
Assume Ht1pair: t ∈ {1,1}.
We prove the intermediate claim Ht1: t = 1.
Apply (UPairE t 1 1 Ht1pair (t = 1)) to the current goal.
Assume H1.
An exact proof term for the current goal is H1.
Assume H1.
An exact proof term for the current goal is H1.
We prove the intermediate claim Hf1: apply_fun normalize01_fun t = 1.
rewrite the current goal using Ht1 (from left to right).
An exact proof term for the current goal is normalize01_fun_1.
We prove the intermediate claim Hbad: Rlt 1 1.
rewrite the current goal using Hf1 (from right to left) at position 1.
An exact proof term for the current goal is Hflt1.
An exact proof term for the current goal is ((not_Rlt_refl 1 real_1) Hbad).
An exact proof term for the current goal is (setminusI R {1,1} t HtR HtNot1).
Let t be given.
Assume Ht: t ∈ R ∖ {1,1}.
We will prove t ∈ W.
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (setminusE1 R {1,1} t Ht).
We prove the intermediate claim HtNot1: t ∉ {1,1}.
An exact proof term for the current goal is (setminusE2 R {1,1} t Ht).
We prove the intermediate claim Htne1: t ≠ 1.
Assume Ht1: t = 1.
We prove the intermediate claim Ht1pair: t ∈ {1,1}.
rewrite the current goal using Ht1 (from left to right).
An exact proof term for the current goal is (UPairI1 1 1).
An exact proof term for the current goal is (HtNot1 Ht1pair).
We prove the intermediate claim Hflt1: Rlt (apply_fun normalize01_fun t) 1.
An exact proof term for the current goal is (normalize01_fun_lt1_of_neq1 t HtR Htne1).
We prove the intermediate claim Hiff: (apply_fun normalize01_fun t ∈ open_ray_lower R 1 ↔ Rlt (apply_fun normalize01_fun t) 1).
An exact proof term for the current goal is (normalize01_fun_img_in_open_ray_lower_iff 1 t real_1 HtR).
We prove the intermediate claim Hray: apply_fun normalize01_fun t ∈ open_ray_lower R 1.
An exact proof term for the current goal is (iffER (apply_fun normalize01_fun t ∈ open_ray_lower R 1) (Rlt (apply_fun normalize01_fun t) 1) Hiff Hflt1).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ apply_fun normalize01_fun x0 ∈ open_ray_lower R 1) t HtR Hray).
We prove the intermediate claim HWdef: preimage_of R normalize01_fun (open_ray_lower R 1) = 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 1 real_1).
∎