Let a and b be given.
Assume Hab: Rle a b.
Assume Hneq: ¬ (a = b).
We will prove ∃h : set, ∃hinv : set, continuous_map (closed_interval a b) (closed_interval_topology a b) (closed_interval (minus_SNo 1) 1) (closed_interval_topology (minus_SNo 1) 1) h ∧ (continuous_map (closed_interval (minus_SNo 1) 1) (closed_interval_topology (minus_SNo 1) 1) (closed_interval a b) (closed_interval_topology a b) hinv ∧ ((∀t : set, t ∈ closed_interval a b → apply_fun hinv (apply_fun h t) = t) ∧ (∀s : set, s ∈ closed_interval (minus_SNo 1) 1 → apply_fun h (apply_fun hinv s) = s))).
Set h to be the term graph R (λt : set ⇒ div_SNo (add_SNo (mul_SNo (add_SNo 1 1) t) (minus_SNo (add_SNo a b))) (add_SNo b (minus_SNo a))).
Set hinv to be the term graph R (λs : set ⇒ div_SNo (add_SNo (mul_SNo (add_SNo b (minus_SNo a)) s) (add_SNo a b)) (add_SNo 1 1)).
We use h to witness the existential quantifier.
We use hinv to witness the existential quantifier.
Apply andI to the current goal.
Set Iab to be the term closed_interval a b.
Set Im1 to be the term closed_interval (minus_SNo 1) 1.
We prove the intermediate claim HIabSub: Iab ⊆ R.
An exact proof term for the current goal is (closed_interval_sub_R a b).
We prove the intermediate claim HIm1Sub: Im1 ⊆ R.
An exact proof term for the current goal is (closed_interval_sub_R (minus_SNo 1) 1).
We prove the intermediate claim HTstd: topology_on R R_standard_topology.
An exact proof term for the current goal is R_standard_topology_is_topology.
We prove the intermediate claim HhR: continuous_map R R_standard_topology R R_standard_topology h.
Set Tx to be the term R_standard_topology.
Set S to be the term open_rays_subbasis R.
We prove the intermediate claim HTx: topology_on R Tx.
An exact proof term for the current goal is R_standard_topology_is_topology.
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (RleE_left a b Hab).
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is (RleE_right a b Hab).
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 HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
Set den to be the term add_SNo b (minus_SNo a).
Set two to be the term add_SNo 1 1.
Set ab to be the term add_SNo a b.
We prove the intermediate claim Hablt: Rlt a b.
An exact proof term for the current goal is (Rle_neq_implies_Rlt a b Hab Hneq).
We prove the intermediate claim H0ltDenR: Rlt 0 den.
An exact proof term for the current goal is (Rlt_0_diff_of_lt a b Hablt).
We prove the intermediate claim HdenPos: 0 < den.
An exact proof term for the current goal is (RltE_lt 0 den H0ltDenR).
We prove the intermediate claim HdenR: den ∈ R.
An exact proof term for the current goal is (real_add_SNo b HbR (minus_SNo a) (real_minus_SNo a HaR)).
We prove the intermediate claim HdenS: SNo den.
An exact proof term for the current goal is (real_SNo den HdenR).
We prove the intermediate claim Hden_ne0: den ≠ 0.
Assume Hden0: den = 0.
We prove the intermediate claim H0lt0S: 0 < 0.
rewrite the current goal using Hden0 (from right to left) at position 2.
An exact proof term for the current goal is HdenPos.
We prove the intermediate claim H0lt0R: Rlt 0 0.
An exact proof term for the current goal is (RltI 0 0 real_0 real_0 H0lt0S).
An exact proof term for the current goal is ((not_Rlt_refl 0 real_0) H0lt0R).
We prove the intermediate claim HtwoS: SNo two.
An exact proof term for the current goal is (SNo_add_SNo 1 1 SNo_1 SNo_1).
We prove the intermediate claim H0lttwo: 0 < two.
We prove the intermediate claim Htwo2: two = 2.
rewrite the current goal using (add_SNo_1_1_2) (from left to right).
Use reflexivity.
rewrite the current goal using Htwo2 (from left to right).
An exact proof term for the current goal is SNoLt_0_2.
We prove the intermediate claim Htwo_ne0: two ≠ 0.
Assume Htwo0: two = 0.
We prove the intermediate claim Htwo2: two = 2.
rewrite the current goal using (add_SNo_1_1_2) (from left to right).
Use reflexivity.
We prove the intermediate claim H20: 2 = 0.
rewrite the current goal using Htwo2 (from right to left) at position 1.
An exact proof term for the current goal is Htwo0.
An exact proof term for the current goal is (neq_2_0 H20).
We prove the intermediate claim HabR: ab ∈ R.
An exact proof term for the current goal is (real_add_SNo a HaR b HbR).
We prove the intermediate claim HabS: SNo ab.
An exact proof term for the current goal is (real_SNo ab HabR).
We prove the intermediate claim Hfun: function_on h R R.
Let t be given.
Assume HtR: t ∈ R.
We will prove apply_fun h t ∈ R.
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
Set num to be the term add_SNo (mul_SNo two t) (minus_SNo ab).
We prove the intermediate claim HnumR: num ∈ R.
We prove the intermediate claim HtwoR: two ∈ R.
An exact proof term for the current goal is (real_add_SNo 1 real_1 1 real_1).
We prove the intermediate claim HmulR: mul_SNo two t ∈ R.
An exact proof term for the current goal is (real_mul_SNo two HtwoR t HtR).
We prove the intermediate claim HabmR: minus_SNo ab ∈ R.
An exact proof term for the current goal is (real_minus_SNo ab HabR).
An exact proof term for the current goal is (real_add_SNo (mul_SNo two t) HmulR (minus_SNo ab) HabmR).
We prove the intermediate claim Hhdef: h = graph R (λt0 : set ⇒ div_SNo (add_SNo (mul_SNo (add_SNo 1 1) t0) (minus_SNo (add_SNo a b))) (add_SNo b (minus_SNo a))).
Use reflexivity.
We prove the intermediate claim Hht: apply_fun h t = div_SNo num den.
rewrite the current goal using Hhdef (from left to right).
rewrite the current goal using (apply_fun_graph R (λt0 : set ⇒ div_SNo (add_SNo (mul_SNo (add_SNo 1 1) t0) (minus_SNo (add_SNo a b))) (add_SNo b (minus_SNo a))) t HtR) (from left to right).
Use reflexivity.
rewrite the current goal using Hht (from left to right).
An exact proof term for the current goal is (real_div_SNo num HnumR den HdenR).
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 = Tx.
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) at position 2.
Apply (continuous_map_from_subbasis R Tx R S h HTx Hfun HS) to the current goal.
Let s be given.
Assume HsS: s ∈ S.
We will prove preimage_of R h s ∈ Tx.
We prove the intermediate claim HSdef: S = (({I ∈ 𝒫 R|∃a0 ∈ R, I = open_ray_upper R a0} ∪ {I ∈ 𝒫 R|∃b0 ∈ R, I = open_ray_lower R b0}) ∪ {R}).
Use reflexivity.
We prove the intermediate claim HsS': s ∈ (({I ∈ 𝒫 R|∃a0 ∈ R, I = open_ray_upper R a0} ∪ {I ∈ 𝒫 R|∃b0 ∈ R, I = open_ray_lower R b0}) ∪ {R}).
rewrite the current goal using HSdef (from right to left).
An exact proof term for the current goal is HsS.
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 R h s ∈ Tx)) to the current goal.
Assume HsAB: 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 R h s ∈ Tx)) to the current goal.
Assume HsUpper: s ∈ {I ∈ 𝒫 R|∃a0 ∈ R, I = open_ray_upper R a0}.
We prove the intermediate claim Hex: ∃c ∈ R, s = open_ray_upper R c.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λI0 : set ⇒ ∃a0 ∈ R, I0 = open_ray_upper R a0) s HsUpper).
Apply Hex to the current goal.
Let c be given.
Assume Hccore.
Apply Hccore to the current goal.
Assume HcR: c ∈ R.
Assume Hseq: s = open_ray_upper R c.
rewrite the current goal using Hseq (from left to right).
Set k to be the term div_SNo (add_SNo (mul_SNo den c) ab) two.
We prove the intermediate claim HkR: k ∈ R.
We prove the intermediate claim HmulR: mul_SNo den c ∈ R.
An exact proof term for the current goal is (real_mul_SNo den HdenR c HcR).
We prove the intermediate claim HnumR: add_SNo (mul_SNo den c) ab ∈ R.
An exact proof term for the current goal is (real_add_SNo (mul_SNo den c) HmulR ab HabR).
An exact proof term for the current goal is (real_div_SNo (add_SNo (mul_SNo den c) ab) HnumR two (real_add_SNo 1 real_1 1 real_1)).
We prove the intermediate claim HkS: SNo k.
An exact proof term for the current goal is (real_SNo k HkR).
We prove the intermediate claim HpreEq: preimage_of R h (open_ray_upper R c) = open_ray_upper R k.
Apply set_ext to the current goal.
Let t be given.
Assume Ht: t ∈ preimage_of R h (open_ray_upper R c).
We will prove t ∈ open_ray_upper R k.
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (SepE1 R (λx : set ⇒ apply_fun h x ∈ open_ray_upper R c) t Ht).
We prove the intermediate claim HhtRay: apply_fun h t ∈ open_ray_upper R c.
An exact proof term for the current goal is (SepE2 R (λx : set ⇒ apply_fun h x ∈ open_ray_upper R c) t Ht).
We prove the intermediate claim Hrel: order_rel R c (apply_fun h t).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R c x0) (apply_fun h t) HhtRay).
We prove the intermediate claim HltR: Rlt c (apply_fun h t).
An exact proof term for the current goal is (order_rel_R_implies_Rlt c (apply_fun h t) Hrel).
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 HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcR).
Set numt to be the term add_SNo (mul_SNo two t) (minus_SNo ab).
We prove the intermediate claim HnumtR: numt ∈ R.
We prove the intermediate claim HtwoR: two ∈ R.
An exact proof term for the current goal is (real_add_SNo 1 real_1 1 real_1).
We prove the intermediate claim HmulR: mul_SNo two t ∈ R.
An exact proof term for the current goal is (real_mul_SNo two HtwoR t HtR).
We prove the intermediate claim HabmR: minus_SNo ab ∈ R.
An exact proof term for the current goal is (real_minus_SNo ab HabR).
An exact proof term for the current goal is (real_add_SNo (mul_SNo two t) HmulR (minus_SNo ab) HabmR).
We prove the intermediate claim HnumtS: SNo numt.
An exact proof term for the current goal is (real_SNo numt HnumtR).
We prove the intermediate claim Hhdef: h = graph R (λt0 : set ⇒ div_SNo (add_SNo (mul_SNo (add_SNo 1 1) t0) (minus_SNo (add_SNo a b))) (add_SNo b (minus_SNo a))).
Use reflexivity.
We prove the intermediate claim Hht: apply_fun h t = div_SNo numt den.
rewrite the current goal using Hhdef (from left to right).
rewrite the current goal using (apply_fun_graph R (λt0 : set ⇒ div_SNo (add_SNo (mul_SNo (add_SNo 1 1) t0) (minus_SNo (add_SNo a b))) (add_SNo b (minus_SNo a))) t HtR) (from left to right).
Use reflexivity.
We prove the intermediate claim HltS: c < apply_fun h t.
An exact proof term for the current goal is (RltE_lt c (apply_fun h t) HltR).
We prove the intermediate claim HdivLt: c < div_SNo numt den.
rewrite the current goal using Hht (from right to left).
An exact proof term for the current goal is HltS.
We prove the intermediate claim HmulLt: mul_SNo c den < numt.
An exact proof term for the current goal is (div_SNo_pos_LtR' numt den c HnumtS HdenS HcS HdenPos HdivLt).
We prove the intermediate claim HmulLt': mul_SNo den c < numt.
rewrite the current goal using (mul_SNo_com den c HdenS HcS) (from left to right) at position 1.
An exact proof term for the current goal is HmulLt.
We prove the intermediate claim HsumLt: add_SNo (mul_SNo den c) ab < add_SNo numt ab.
An exact proof term for the current goal is (add_SNo_Lt1 (mul_SNo den c) ab numt (SNo_mul_SNo den c HdenS HcS) HabS HnumtS HmulLt').
We prove the intermediate claim HrightEq: add_SNo numt ab = mul_SNo two t.
We prove the intermediate claim Hnumdef: numt = add_SNo (mul_SNo two t) (minus_SNo ab).
Use reflexivity.
rewrite the current goal using Hnumdef (from left to right).
An exact proof term for the current goal is (add_SNo_minus_R2' (mul_SNo two t) ab (SNo_mul_SNo two t HtwoS HtS) HabS).
We prove the intermediate claim Hlt2t: add_SNo (mul_SNo den c) ab < mul_SNo two t.
rewrite the current goal using HrightEq (from right to left) at position 1.
An exact proof term for the current goal is HsumLt.
We prove the intermediate claim Hlt_t2: add_SNo (mul_SNo den c) ab < mul_SNo t two.
rewrite the current goal using (mul_SNo_com two t HtwoS HtS) (from right to left).
An exact proof term for the current goal is Hlt2t.
We prove the intermediate claim Hklt: k < t.
An exact proof term for the current goal is (div_SNo_pos_LtL (add_SNo (mul_SNo den c) ab) two t (SNo_add_SNo (mul_SNo den c) ab (SNo_mul_SNo den c HdenS HcS) HabS) HtwoS HtS H0lttwo Hlt_t2).
We prove the intermediate claim HkltR: Rlt k t.
An exact proof term for the current goal is (RltI k t HkR HtR Hklt).
We prove the intermediate claim Hrelkt: order_rel R k t.
An exact proof term for the current goal is (Rlt_implies_order_rel_R k t HkltR).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R k x0) t HtR Hrelkt).
Let t be given.
Assume Ht: t ∈ open_ray_upper R k.
We will prove t ∈ preimage_of R h (open_ray_upper R c).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ order_rel R k x0) t Ht).
We prove the intermediate claim Hrelkt: order_rel R k t.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R k x0) t Ht).
We prove the intermediate claim HltR: Rlt k t.
An exact proof term for the current goal is (order_rel_R_implies_Rlt k t Hrelkt).
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 HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcR).
We prove the intermediate claim HkS: SNo k.
An exact proof term for the current goal is (real_SNo k HkR).
We prove the intermediate claim HltS: k < t.
An exact proof term for the current goal is (RltE_lt k t HltR).
We prove the intermediate claim HmulLt: add_SNo (mul_SNo den c) ab < mul_SNo t two.
An exact proof term for the current goal is (div_SNo_pos_LtL' (add_SNo (mul_SNo den c) ab) two t (SNo_add_SNo (mul_SNo den c) ab (SNo_mul_SNo den c HdenS HcS) HabS) HtwoS HtS H0lttwo HltS).
We prove the intermediate claim HmulLt2: add_SNo (mul_SNo den c) ab < mul_SNo two t.
rewrite the current goal using (mul_SNo_com two t HtwoS HtS) (from left to right).
An exact proof term for the current goal is HmulLt.
Set numt to be the term add_SNo (mul_SNo two t) (minus_SNo ab).
We prove the intermediate claim HnumtS: SNo numt.
An exact proof term for the current goal is (SNo_add_SNo (mul_SNo two t) (minus_SNo ab) (SNo_mul_SNo two t HtwoS HtS) (SNo_minus_SNo ab HabS)).
We prove the intermediate claim HrhsLt: mul_SNo den c < numt.
We prove the intermediate claim HrightEq: add_SNo numt ab = mul_SNo two t.
We prove the intermediate claim Hnumdef: numt = add_SNo (mul_SNo two t) (minus_SNo ab).
Use reflexivity.
rewrite the current goal using Hnumdef (from left to right).
An exact proof term for the current goal is (add_SNo_minus_R2' (mul_SNo two t) ab (SNo_mul_SNo two t HtwoS HtS) HabS).
We prove the intermediate claim HsumLt': add_SNo (mul_SNo den c) ab < add_SNo numt ab.
rewrite the current goal using HrightEq (from left to right).
An exact proof term for the current goal is HmulLt2.
An exact proof term for the current goal is (add_SNo_Lt1_cancel (mul_SNo den c) ab numt (SNo_mul_SNo den c HdenS HcS) HabS HnumtS HsumLt').
We prove the intermediate claim HrhsLt': mul_SNo c den < numt.
rewrite the current goal using (mul_SNo_com c den HcS HdenS) (from left to right).
An exact proof term for the current goal is HrhsLt.
We prove the intermediate claim HdivLt: c < div_SNo numt den.
An exact proof term for the current goal is (div_SNo_pos_LtR numt den c HnumtS HdenS HcS HdenPos HrhsLt').
We prove the intermediate claim Hhdef: h = graph R (λt0 : set ⇒ div_SNo (add_SNo (mul_SNo (add_SNo 1 1) t0) (minus_SNo (add_SNo a b))) (add_SNo b (minus_SNo a))).
Use reflexivity.
We prove the intermediate claim Hht: apply_fun h t = div_SNo numt den.
rewrite the current goal using Hhdef (from left to right).
rewrite the current goal using (apply_fun_graph R (λt0 : set ⇒ div_SNo (add_SNo (mul_SNo (add_SNo 1 1) t0) (minus_SNo (add_SNo a b))) (add_SNo b (minus_SNo a))) t HtR) (from left to right).
Use reflexivity.
We prove the intermediate claim HcLtHtS: c < apply_fun h t.
rewrite the current goal using Hht (from left to right).
An exact proof term for the current goal is HdivLt.
We prove the intermediate claim HhtR: apply_fun h t ∈ R.
An exact proof term for the current goal is (Hfun t HtR).
We prove the intermediate claim HcLtHtR: Rlt c (apply_fun h t).
An exact proof term for the current goal is (RltI c (apply_fun h t) HcR HhtR HcLtHtS).
We prove the intermediate claim Hrelct: order_rel R c (apply_fun h t).
An exact proof term for the current goal is (Rlt_implies_order_rel_R c (apply_fun h t) HcLtHtR).
We prove the intermediate claim HhtRay: apply_fun h t ∈ open_ray_upper R c.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R c x0) (apply_fun h t) HhtR Hrelct).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ apply_fun h x0 ∈ open_ray_upper R c) t HtR HhtRay).
rewrite the current goal using HpreEq (from left to right).
rewrite the current goal using standard_topology_is_order_topology (from right to left).
We prove the intermediate claim HsRay: open_ray_upper R k ∈ open_rays_subbasis R.
An exact proof term for the current goal is (open_ray_upper_in_open_rays_subbasis R k HkR).
An exact proof term for the current goal is (open_rays_subbasis_sub_order_topology_R (open_ray_upper R k) HsRay).
Assume HsLower: s ∈ {I ∈ 𝒫 R|∃b0 ∈ R, I = open_ray_lower R b0}.
We prove the intermediate claim Hex: ∃c ∈ R, s = open_ray_lower R c.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λI0 : set ⇒ ∃b0 ∈ R, I0 = open_ray_lower R b0) s HsLower).
Apply Hex to the current goal.
Let c be given.
Assume Hccore.
Apply Hccore to the current goal.
Assume HcR: c ∈ R.
Assume Hseq: s = open_ray_lower R c.
rewrite the current goal using Hseq (from left to right).
Set k to be the term div_SNo (add_SNo (mul_SNo den c) ab) two.
We prove the intermediate claim HkR: k ∈ R.
We prove the intermediate claim HmulR: mul_SNo den c ∈ R.
An exact proof term for the current goal is (real_mul_SNo den HdenR c HcR).
We prove the intermediate claim HnumR: add_SNo (mul_SNo den c) ab ∈ R.
An exact proof term for the current goal is (real_add_SNo (mul_SNo den c) HmulR ab HabR).
An exact proof term for the current goal is (real_div_SNo (add_SNo (mul_SNo den c) ab) HnumR two (real_add_SNo 1 real_1 1 real_1)).
We prove the intermediate claim HkS: SNo k.
An exact proof term for the current goal is (real_SNo k HkR).
We prove the intermediate claim HpreEq: preimage_of R h (open_ray_lower R c) = open_ray_lower R k.
Apply set_ext to the current goal.
Let t be given.
Assume Ht: t ∈ preimage_of R h (open_ray_lower R c).
We will prove t ∈ open_ray_lower R k.
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (SepE1 R (λx : set ⇒ apply_fun h x ∈ open_ray_lower R c) t Ht).
We prove the intermediate claim HhtRay: apply_fun h t ∈ open_ray_lower R c.
An exact proof term for the current goal is (SepE2 R (λx : set ⇒ apply_fun h x ∈ open_ray_lower R c) t Ht).
We prove the intermediate claim Hrel: order_rel R (apply_fun h t) c.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R x0 c) (apply_fun h t) HhtRay).
We prove the intermediate claim HltR: Rlt (apply_fun h t) c.
An exact proof term for the current goal is (order_rel_R_implies_Rlt (apply_fun h t) c Hrel).
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 HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcR).
Set numt to be the term add_SNo (mul_SNo two t) (minus_SNo ab).
We prove the intermediate claim HnumtR: numt ∈ R.
We prove the intermediate claim HtwoR: two ∈ R.
An exact proof term for the current goal is (real_add_SNo 1 real_1 1 real_1).
We prove the intermediate claim HmulR: mul_SNo two t ∈ R.
An exact proof term for the current goal is (real_mul_SNo two HtwoR t HtR).
We prove the intermediate claim HabmR: minus_SNo ab ∈ R.
An exact proof term for the current goal is (real_minus_SNo ab HabR).
An exact proof term for the current goal is (real_add_SNo (mul_SNo two t) HmulR (minus_SNo ab) HabmR).
We prove the intermediate claim HnumtS: SNo numt.
An exact proof term for the current goal is (real_SNo numt HnumtR).
We prove the intermediate claim Hhdef: h = graph R (λt0 : set ⇒ div_SNo (add_SNo (mul_SNo (add_SNo 1 1) t0) (minus_SNo (add_SNo a b))) (add_SNo b (minus_SNo a))).
Use reflexivity.
We prove the intermediate claim Hht: apply_fun h t = div_SNo numt den.
rewrite the current goal using Hhdef (from left to right).
rewrite the current goal using (apply_fun_graph R (λt0 : set ⇒ div_SNo (add_SNo (mul_SNo (add_SNo 1 1) t0) (minus_SNo (add_SNo a b))) (add_SNo b (minus_SNo a))) t HtR) (from left to right).
Use reflexivity.
We prove the intermediate claim HltS: apply_fun h t < c.
An exact proof term for the current goal is (RltE_lt (apply_fun h t) c HltR).
We prove the intermediate claim HdivLt: div_SNo numt den < c.
rewrite the current goal using Hht (from right to left).
An exact proof term for the current goal is HltS.
We prove the intermediate claim HrhsLt: numt < mul_SNo c den.
An exact proof term for the current goal is (div_SNo_pos_LtL' numt den c HnumtS HdenS HcS HdenPos HdivLt).
We prove the intermediate claim HrhsLt': numt < mul_SNo den c.
rewrite the current goal using (mul_SNo_com den c HdenS HcS) (from left to right).
An exact proof term for the current goal is HrhsLt.
We prove the intermediate claim HsumLt: add_SNo numt ab < add_SNo (mul_SNo den c) ab.
An exact proof term for the current goal is (add_SNo_Lt1 numt ab (mul_SNo den c) HnumtS HabS (SNo_mul_SNo den c HdenS HcS) HrhsLt').
We prove the intermediate claim HleftEq: add_SNo numt ab = mul_SNo two t.
We prove the intermediate claim Hnumdef: numt = add_SNo (mul_SNo two t) (minus_SNo ab).
Use reflexivity.
rewrite the current goal using Hnumdef (from left to right).
An exact proof term for the current goal is (add_SNo_minus_R2' (mul_SNo two t) ab (SNo_mul_SNo two t HtwoS HtS) HabS).
We prove the intermediate claim Hlt2t: mul_SNo two t < add_SNo (mul_SNo den c) ab.
rewrite the current goal using HleftEq (from right to left) at position 1.
An exact proof term for the current goal is HsumLt.
We prove the intermediate claim Hlt_t2: mul_SNo t two < add_SNo (mul_SNo den c) ab.
rewrite the current goal using (mul_SNo_com t two HtS HtwoS) (from left to right).
An exact proof term for the current goal is Hlt2t.
We prove the intermediate claim Htlt: t < k.
An exact proof term for the current goal is (div_SNo_pos_LtR (add_SNo (mul_SNo den c) ab) two t (SNo_add_SNo (mul_SNo den c) ab (SNo_mul_SNo den c HdenS HcS) HabS) HtwoS HtS H0lttwo Hlt_t2).
We prove the intermediate claim HtltR: Rlt t k.
An exact proof term for the current goal is (RltI t k HtR HkR Htlt).
We prove the intermediate claim Hreltk: order_rel R t k.
An exact proof term for the current goal is (Rlt_implies_order_rel_R t k HtltR).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R x0 k) t HtR Hreltk).
Let t be given.
Assume Ht: t ∈ open_ray_lower R k.
We will prove t ∈ preimage_of R h (open_ray_lower R c).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ order_rel R x0 k) t Ht).
We prove the intermediate claim Hreltk: order_rel R t k.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R x0 k) t Ht).
We prove the intermediate claim HltR: Rlt t k.
An exact proof term for the current goal is (order_rel_R_implies_Rlt t k Hreltk).
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 HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcR).
We prove the intermediate claim HkS: SNo k.
An exact proof term for the current goal is (real_SNo k HkR).
We prove the intermediate claim HltS: t < k.
An exact proof term for the current goal is (RltE_lt t k HltR).
We prove the intermediate claim HmulLt: mul_SNo t two < add_SNo (mul_SNo den c) ab.
An exact proof term for the current goal is (div_SNo_pos_LtR' (add_SNo (mul_SNo den c) ab) two t (SNo_add_SNo (mul_SNo den c) ab (SNo_mul_SNo den c HdenS HcS) HabS) HtwoS HtS H0lttwo HltS).
We prove the intermediate claim HmulLt2: mul_SNo two t < add_SNo (mul_SNo den c) ab.
rewrite the current goal using (mul_SNo_com two t HtwoS HtS) (from left to right).
An exact proof term for the current goal is HmulLt.
We prove the intermediate claim HmulLt2c: mul_SNo two t < add_SNo (mul_SNo c den) ab.
rewrite the current goal using (mul_SNo_com c den HcS HdenS) (from left to right).
An exact proof term for the current goal is HmulLt2.
Set numt to be the term add_SNo (mul_SNo two t) (minus_SNo ab).
We prove the intermediate claim HnumtS: SNo numt.
An exact proof term for the current goal is (SNo_add_SNo (mul_SNo two t) (minus_SNo ab) (SNo_mul_SNo two t HtwoS HtS) (SNo_minus_SNo ab HabS)).
We prove the intermediate claim HrhsLt: numt < mul_SNo c den.
We prove the intermediate claim HleftEq: add_SNo numt ab = mul_SNo two t.
We prove the intermediate claim Hnumdef: numt = add_SNo (mul_SNo two t) (minus_SNo ab).
Use reflexivity.
rewrite the current goal using Hnumdef (from left to right).
An exact proof term for the current goal is (add_SNo_minus_R2' (mul_SNo two t) ab (SNo_mul_SNo two t HtwoS HtS) HabS).
We prove the intermediate claim HsumLt': add_SNo numt ab < add_SNo (mul_SNo c den) ab.
rewrite the current goal using HleftEq (from left to right).
An exact proof term for the current goal is HmulLt2c.
An exact proof term for the current goal is (add_SNo_Lt1_cancel numt ab (mul_SNo c den) HnumtS HabS (SNo_mul_SNo c den HcS HdenS) HsumLt').
We prove the intermediate claim HdivLt: div_SNo numt den < c.
An exact proof term for the current goal is (div_SNo_pos_LtL numt den c HnumtS HdenS HcS HdenPos HrhsLt).
We prove the intermediate claim Hhdef: h = graph R (λt0 : set ⇒ div_SNo (add_SNo (mul_SNo (add_SNo 1 1) t0) (minus_SNo (add_SNo a b))) (add_SNo b (minus_SNo a))).
Use reflexivity.
We prove the intermediate claim Hht: apply_fun h t = div_SNo numt den.
rewrite the current goal using Hhdef (from left to right).
rewrite the current goal using (apply_fun_graph R (λt0 : set ⇒ div_SNo (add_SNo (mul_SNo (add_SNo 1 1) t0) (minus_SNo (add_SNo a b))) (add_SNo b (minus_SNo a))) t HtR) (from left to right).
Use reflexivity.
We prove the intermediate claim HhtR: apply_fun h t ∈ R.
An exact proof term for the current goal is (Hfun t HtR).
We prove the intermediate claim HhtLtC: apply_fun h t < c.
rewrite the current goal using Hht (from left to right).
An exact proof term for the current goal is HdivLt.
We prove the intermediate claim HhtLtCR: Rlt (apply_fun h t) c.
An exact proof term for the current goal is (RltI (apply_fun h t) c HhtR HcR HhtLtC).
We prove the intermediate claim Hrelct: order_rel R (apply_fun h t) c.
An exact proof term for the current goal is (Rlt_implies_order_rel_R (apply_fun h t) c HhtLtCR).
We prove the intermediate claim HhtRay: apply_fun h t ∈ open_ray_lower R c.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R x0 c) (apply_fun h t) HhtR Hrelct).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ apply_fun h x0 ∈ open_ray_lower R c) t HtR HhtRay).
rewrite the current goal using HpreEq (from left to right).
rewrite the current goal using standard_topology_is_order_topology (from right to left).
We prove the intermediate claim HsRay: open_ray_lower R k ∈ open_rays_subbasis R.
An exact proof term for the current goal is (open_ray_lower_in_open_rays_subbasis R k HkR).
An exact proof term for the current goal is (open_rays_subbasis_sub_order_topology_R (open_ray_lower R k) HsRay).
An exact proof term for the current goal is HsAB.
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).
rewrite the current goal using (preimage_of_whole R R h Hfun) (from left to right).
An exact proof term for the current goal is (topology_has_X R Tx HTx).
An exact proof term for the current goal is HsS'.
We prove the intermediate claim HhDom: continuous_map Iab (subspace_topology R R_standard_topology Iab) R R_standard_topology h.
An exact proof term for the current goal is (continuous_on_subspace_rule R R_standard_topology R R_standard_topology h Iab HTstd HTstd HIabSub HhR).
We prove the intermediate claim HhImg: ∀x : set, x ∈ Iab → apply_fun h x ∈ Im1.
Let x be given.
Assume HxI: x ∈ Iab.
We will prove apply_fun h x ∈ Im1.
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (RleE_left a b Hab).
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is (RleE_right a b Hab).
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 HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (HIabSub x HxI).
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
We prove the intermediate claim Hbounds: Rle a x ∧ Rle x b.
An exact proof term for the current goal is (closed_interval_bounds a b x HaR HbR HxI).
We prove the intermediate claim Hax: Rle a x.
An exact proof term for the current goal is (andEL (Rle a x) (Rle x b) Hbounds).
We prove the intermediate claim Hxb: Rle x b.
An exact proof term for the current goal is (andER (Rle a x) (Rle x b) Hbounds).
Set den to be the term add_SNo b (minus_SNo a).
Set two to be the term add_SNo 1 1.
Set ab to be the term add_SNo a b.
Set num to be the term add_SNo (mul_SNo two x) (minus_SNo ab).
We prove the intermediate claim HdenR: den ∈ R.
An exact proof term for the current goal is (real_add_SNo b HbR (minus_SNo a) (real_minus_SNo a HaR)).
We prove the intermediate claim HdenS: SNo den.
An exact proof term for the current goal is (real_SNo den HdenR).
We prove the intermediate claim HtwoS: SNo two.
An exact proof term for the current goal is (SNo_add_SNo 1 1 SNo_1 SNo_1).
We prove the intermediate claim Htwo_ne0: two ≠ 0.
Assume Htwo0: two = 0.
We prove the intermediate claim Htwo2: two = 2.
rewrite the current goal using (add_SNo_1_1_2) (from left to right).
Use reflexivity.
We prove the intermediate claim H20: 2 = 0.
rewrite the current goal using Htwo2 (from right to left) at position 1.
An exact proof term for the current goal is Htwo0.
An exact proof term for the current goal is (neq_2_0 H20).
We prove the intermediate claim Hablt: Rlt a b.
An exact proof term for the current goal is (Rle_neq_implies_Rlt a b Hab Hneq).
We prove the intermediate claim H0ltDenR: Rlt 0 den.
An exact proof term for the current goal is (Rlt_0_diff_of_lt a b Hablt).
We prove the intermediate claim HdenPos: 0 < den.
An exact proof term for the current goal is (RltE_lt 0 den H0ltDenR).
We prove the intermediate claim Hden_ne0: den ≠ 0.
Assume Hden0: den = 0.
We prove the intermediate claim H0lt0S: 0 < 0.
rewrite the current goal using Hden0 (from right to left) at position 2.
An exact proof term for the current goal is HdenPos.
We prove the intermediate claim H0lt0R: Rlt 0 0.
An exact proof term for the current goal is (RltI 0 0 real_0 real_0 H0lt0S).
An exact proof term for the current goal is ((not_Rlt_refl 0 real_0) H0lt0R).
We prove the intermediate claim HabR: ab ∈ R.
An exact proof term for the current goal is (real_add_SNo a HaR b HbR).
We prove the intermediate claim HabS: SNo ab.
An exact proof term for the current goal is (real_SNo ab HabR).
We prove the intermediate claim HnumR: num ∈ R.
We prove the intermediate claim HtwoR: two ∈ R.
An exact proof term for the current goal is (real_add_SNo 1 real_1 1 real_1).
We prove the intermediate claim HmulR: mul_SNo two x ∈ R.
An exact proof term for the current goal is (real_mul_SNo two HtwoR x HxR).
We prove the intermediate claim HabmR: minus_SNo ab ∈ R.
An exact proof term for the current goal is (real_minus_SNo ab HabR).
An exact proof term for the current goal is (real_add_SNo (mul_SNo two x) HmulR (minus_SNo ab) HabmR).
We prove the intermediate claim HnumS: SNo num.
An exact proof term for the current goal is (real_SNo num HnumR).
We prove the intermediate claim Hhdef: h = graph R (λt0 : set ⇒ div_SNo (add_SNo (mul_SNo (add_SNo 1 1) t0) (minus_SNo (add_SNo a b))) (add_SNo b (minus_SNo a))).
Use reflexivity.
We prove the intermediate claim Hhx: apply_fun h x = div_SNo num den.
rewrite the current goal using Hhdef (from left to right).
rewrite the current goal using (apply_fun_graph R (λt0 : set ⇒ div_SNo (add_SNo (mul_SNo (add_SNo 1 1) t0) (minus_SNo (add_SNo a b))) (add_SNo b (minus_SNo a))) x HxR) (from left to right).
Use reflexivity.
We prove the intermediate claim HhxR: apply_fun h x ∈ R.
rewrite the current goal using Hhx (from left to right).
An exact proof term for the current goal is (real_div_SNo num HnumR den HdenR).
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 Hlo: Rle (minus_SNo 1) (apply_fun h x).
Apply (RleI (minus_SNo 1) (apply_fun h x) Hm1R HhxR) to the current goal.
Assume Hlt: Rlt (apply_fun h x) (minus_SNo 1).
We prove the intermediate claim HltS: apply_fun h x < minus_SNo 1.
An exact proof term for the current goal is (RltE_lt (apply_fun h x) (minus_SNo 1) Hlt).
We prove the intermediate claim HdivLt: div_SNo num den < minus_SNo 1.
rewrite the current goal using Hhx (from right to left).
An exact proof term for the current goal is HltS.
We prove the intermediate claim Hm1S: SNo (minus_SNo 1).
An exact proof term for the current goal is (SNo_minus_SNo 1 SNo_1).
We prove the intermediate claim HnumLt: num < mul_SNo (minus_SNo 1) den.
An exact proof term for the current goal is (div_SNo_pos_LtL' num den (minus_SNo 1) HnumS HdenS Hm1S HdenPos HdivLt).
We prove the intermediate claim Hm1denEq: mul_SNo (minus_SNo 1) den = add_SNo a (minus_SNo b).
We prove the intermediate claim Hm1den: mul_SNo (minus_SNo 1) den = minus_SNo den.
We prove the intermediate claim Hcomm: mul_SNo (minus_SNo 1) den = mul_SNo den (minus_SNo 1).
An exact proof term for the current goal is (mul_SNo_com (minus_SNo 1) den (SNo_minus_SNo 1 SNo_1) HdenS).
rewrite the current goal using Hcomm (from left to right).
rewrite the current goal using (mul_SNo_minus_distrR den 1 HdenS SNo_1) (from left to right).
rewrite the current goal using (mul_SNo_oneR den HdenS) (from left to right).
Use reflexivity.
rewrite the current goal using Hm1den (from left to right).
rewrite the current goal using (minus_add_SNo_distr b (minus_SNo a) HbS (SNo_minus_SNo a HaS)) (from left to right).
rewrite the current goal using (minus_SNo_minus_SNo_real a HaR) (from left to right).
We prove the intermediate claim Hcom: add_SNo (minus_SNo b) a = add_SNo a (minus_SNo b).
An exact proof term for the current goal is (add_SNo_com (minus_SNo b) a (SNo_minus_SNo b HbS) HaS).
rewrite the current goal using Hcom (from left to right).
Use reflexivity.
We prove the intermediate claim HrhsS: SNo (add_SNo a (minus_SNo b)).
An exact proof term for the current goal is (SNo_add_SNo a (minus_SNo b) HaS (SNo_minus_SNo b HbS)).
We prove the intermediate claim HnumLt2: num < add_SNo a (minus_SNo b).
rewrite the current goal using Hm1denEq (from right to left) at position 1.
An exact proof term for the current goal is HnumLt.
We prove the intermediate claim HsumLt: add_SNo num ab < add_SNo (add_SNo a (minus_SNo b)) ab.
An exact proof term for the current goal is (add_SNo_Lt1 num ab (add_SNo a (minus_SNo b)) HnumS HabS HrhsS HnumLt2).
We prove the intermediate claim HleftEq: add_SNo num ab = mul_SNo two x.
We prove the intermediate claim Hnumdef: num = add_SNo (mul_SNo two x) (minus_SNo ab).
Use reflexivity.
rewrite the current goal using Hnumdef (from left to right).
An exact proof term for the current goal is (add_SNo_minus_R2' (mul_SNo two x) ab (SNo_mul_SNo two x HtwoS HxS) HabS).
We prove the intermediate claim HrightEq: add_SNo (add_SNo a (minus_SNo b)) ab = mul_SNo two a.
We prove the intermediate claim Habdef: ab = add_SNo a b.
Use reflexivity.
rewrite the current goal using Habdef (from left to right).
We prove the intermediate claim Hmul2a: mul_SNo two a = add_SNo a a.
We prove the intermediate claim HtwoDef: two = add_SNo 1 1.
Use reflexivity.
rewrite the current goal using HtwoDef (from left to right).
rewrite the current goal using (mul_SNo_distrR 1 1 a SNo_1 SNo_1 HaS) (from left to right).
rewrite the current goal using (mul_SNo_oneL a HaS) (from left to right) at position 1.
rewrite the current goal using (mul_SNo_oneL a HaS) (from left to right).
Use reflexivity.
rewrite the current goal using Hmul2a (from left to right).
rewrite the current goal using (add_SNo_assoc (add_SNo a (minus_SNo b)) a b (SNo_add_SNo a (minus_SNo b) HaS (SNo_minus_SNo b HbS)) HaS HbS) (from left to right).
rewrite the current goal using (add_SNo_com_3b_1_2 a (minus_SNo b) a HaS (SNo_minus_SNo b HbS) HaS) (from left to right) at position 1.
rewrite the current goal using (add_SNo_assoc (add_SNo a a) (minus_SNo b) b (SNo_add_SNo a a HaS HaS) (SNo_minus_SNo b HbS) HbS) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_linv b HbS) (from left to right).
rewrite the current goal using (add_SNo_0R (add_SNo a a) (SNo_add_SNo a a HaS HaS)) (from left to right).
Use reflexivity.
We prove the intermediate claim H2xLt: mul_SNo two x < mul_SNo two a.
rewrite the current goal using HleftEq (from right to left) at position 1.
rewrite the current goal using HrightEq (from right to left) at position 1.
An exact proof term for the current goal is HsumLt.
We prove the intermediate claim H2xLt': mul_SNo two x < mul_SNo a two.
rewrite the current goal using (mul_SNo_com a two HaS HtwoS) (from left to right) at position 1.
An exact proof term for the current goal is H2xLt.
We prove the intermediate claim H0lttwo: 0 < two.
We prove the intermediate claim Htwo2: two = 2.
rewrite the current goal using (add_SNo_1_1_2) (from left to right).
Use reflexivity.
rewrite the current goal using Htwo2 (from left to right).
An exact proof term for the current goal is SNoLt_0_2.
We prove the intermediate claim HxLtA: div_SNo (mul_SNo two x) two < a.
An exact proof term for the current goal is (div_SNo_pos_LtL (mul_SNo two x) two a (SNo_mul_SNo two x HtwoS HxS) HtwoS HaS H0lttwo H2xLt').
We prove the intermediate claim HdivEq: div_SNo (mul_SNo two x) two = x.
We prove the intermediate claim HmulId: mul_SNo two x = mul_SNo two x.
Use reflexivity.
An exact proof term for the current goal is (mul_div_SNo_nonzero_eq (mul_SNo two x) two x (SNo_mul_SNo two x HtwoS HxS) HtwoS HxS Htwo_ne0 HmulId).
We prove the intermediate claim HxLtAS: x < a.
rewrite the current goal using HdivEq (from right to left) at position 1.
An exact proof term for the current goal is HxLtA.
We prove the intermediate claim HxLtAR: Rlt x a.
An exact proof term for the current goal is (RltI x a HxR HaR HxLtAS).
An exact proof term for the current goal is ((RleE_nlt a x Hax) HxLtAR).
We prove the intermediate claim Hhi: Rle (apply_fun h x) 1.
Apply (RleI (apply_fun h x) 1 HhxR real_1) to the current goal.
Assume Hlt: Rlt 1 (apply_fun h x).
We prove the intermediate claim HltS: 1 < apply_fun h x.
An exact proof term for the current goal is (RltE_lt 1 (apply_fun h x) Hlt).
We prove the intermediate claim HdivLt: 1 < div_SNo num den.
rewrite the current goal using Hhx (from right to left).
An exact proof term for the current goal is HltS.
We prove the intermediate claim HnumGt: mul_SNo 1 den < num.
An exact proof term for the current goal is (div_SNo_pos_LtR' num den 1 HnumS HdenS SNo_1 HdenPos HdivLt).
We prove the intermediate claim HdenEq: mul_SNo 1 den = den.
An exact proof term for the current goal is (mul_SNo_oneL den HdenS).
We prove the intermediate claim HdenLtNum: den < num.
rewrite the current goal using HdenEq (from right to left) at position 1.
An exact proof term for the current goal is HnumGt.
We prove the intermediate claim HsumLt: add_SNo den ab < add_SNo num ab.
An exact proof term for the current goal is (add_SNo_Lt1 den ab num HdenS HabS HnumS HdenLtNum).
We prove the intermediate claim HleftEq: add_SNo den ab = mul_SNo two b.
We prove the intermediate claim Hdendef: den = add_SNo b (minus_SNo a).
Use reflexivity.
We prove the intermediate claim Habdef: ab = add_SNo a b.
Use reflexivity.
rewrite the current goal using Hdendef (from left to right).
rewrite the current goal using Habdef (from left to right).
rewrite the current goal using (add_SNo_assoc (add_SNo b (minus_SNo a)) a b (SNo_add_SNo b (minus_SNo a) HbS (SNo_minus_SNo a HaS)) HaS HbS) (from left to right).
rewrite the current goal using (add_SNo_com_3b_1_2 b (minus_SNo a) a HbS (SNo_minus_SNo a HaS) HaS) (from left to right) at position 1.
rewrite the current goal using (add_SNo_minus_R2 b a HbS HaS) (from left to right) at position 1.
We prove the intermediate claim Hmul2b: mul_SNo two b = add_SNo b b.
We prove the intermediate claim HtwoDef: two = add_SNo 1 1.
Use reflexivity.
rewrite the current goal using HtwoDef (from left to right).
rewrite the current goal using (mul_SNo_distrR 1 1 b SNo_1 SNo_1 HbS) (from left to right).
rewrite the current goal using (mul_SNo_oneL b HbS) (from left to right) at position 1.
rewrite the current goal using (mul_SNo_oneL b HbS) (from left to right).
Use reflexivity.
rewrite the current goal using Hmul2b (from left to right).
Use reflexivity.
We prove the intermediate claim HrightEq: add_SNo num ab = mul_SNo two x.
We prove the intermediate claim Hnumdef: num = add_SNo (mul_SNo two x) (minus_SNo ab).
Use reflexivity.
rewrite the current goal using Hnumdef (from left to right).
An exact proof term for the current goal is (add_SNo_minus_R2' (mul_SNo two x) ab (SNo_mul_SNo two x HtwoS HxS) HabS).
We prove the intermediate claim H2bLt2x: mul_SNo two b < mul_SNo two x.
rewrite the current goal using HleftEq (from right to left) at position 1.
rewrite the current goal using HrightEq (from right to left) at position 1.
An exact proof term for the current goal is HsumLt.
We prove the intermediate claim H2bLt2x': mul_SNo b two < mul_SNo two x.
rewrite the current goal using (mul_SNo_com b two HbS HtwoS) (from left to right) at position 1.
An exact proof term for the current goal is H2bLt2x.
We prove the intermediate claim H0lttwo: 0 < two.
We prove the intermediate claim Htwo2: two = 2.
rewrite the current goal using (add_SNo_1_1_2) (from left to right).
Use reflexivity.
rewrite the current goal using Htwo2 (from left to right).
An exact proof term for the current goal is SNoLt_0_2.
We prove the intermediate claim HbLtX: b < div_SNo (mul_SNo two x) two.
An exact proof term for the current goal is (div_SNo_pos_LtR (mul_SNo two x) two b (SNo_mul_SNo two x HtwoS HxS) HtwoS HbS H0lttwo H2bLt2x').
We prove the intermediate claim HdivEq: div_SNo (mul_SNo two x) two = x.
We prove the intermediate claim HmulId: mul_SNo two x = mul_SNo two x.
Use reflexivity.
An exact proof term for the current goal is (mul_div_SNo_nonzero_eq (mul_SNo two x) two x (SNo_mul_SNo two x HtwoS HxS) HtwoS HxS Htwo_ne0 HmulId).
We prove the intermediate claim HbLtX': b < x.
rewrite the current goal using HdivEq (from right to left) at position 1.
An exact proof term for the current goal is HbLtX.
We prove the intermediate claim HbLtXR: Rlt b x.
An exact proof term for the current goal is (RltI b x HbR HxR HbLtX').
An exact proof term for the current goal is ((RleE_nlt x b Hxb) HbLtXR).
An exact proof term for the current goal is (closed_intervalI_of_Rle (minus_SNo 1) 1 (apply_fun h x) Hm1R real_1 HhxR Hlo Hhi).
We prove the intermediate claim HhCod: continuous_map Iab (subspace_topology R R_standard_topology Iab) Im1 (subspace_topology R R_standard_topology Im1) h.
An exact proof term for the current goal is (continuous_map_range_restrict Iab (subspace_topology R R_standard_topology Iab) R R_standard_topology h Im1 HhDom HIm1Sub HhImg).
We prove the intermediate claim HTiabEq: closed_interval_topology a b = subspace_topology R R_standard_topology Iab.
Use reflexivity.
We prove the intermediate claim HTim1Eq: closed_interval_topology (minus_SNo 1) 1 = subspace_topology R R_standard_topology Im1.
Use reflexivity.
rewrite the current goal using HTiabEq (from left to right).
rewrite the current goal using HTim1Eq (from left to right).
An exact proof term for the current goal is HhCod.
Apply andI to the current goal.
Set Iab to be the term closed_interval a b.
Set Im1 to be the term closed_interval (minus_SNo 1) 1.
We prove the intermediate claim HIabSub: Iab ⊆ R.
An exact proof term for the current goal is (closed_interval_sub_R a b).
We prove the intermediate claim HIm1Sub: Im1 ⊆ R.
An exact proof term for the current goal is (closed_interval_sub_R (minus_SNo 1) 1).
We prove the intermediate claim HTstd: topology_on R R_standard_topology.
An exact proof term for the current goal is R_standard_topology_is_topology.
We prove the intermediate claim HhinvR: continuous_map R R_standard_topology R R_standard_topology hinv.
Set Tx to be the term R_standard_topology.
Set S to be the term open_rays_subbasis R.
We prove the intermediate claim HTx: topology_on R Tx.
An exact proof term for the current goal is R_standard_topology_is_topology.
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (RleE_left a b Hab).
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is (RleE_right a b Hab).
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 HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
Set den to be the term add_SNo b (minus_SNo a).
Set two to be the term add_SNo 1 1.
Set ab to be the term add_SNo a b.
We prove the intermediate claim Hablt: Rlt a b.
An exact proof term for the current goal is (Rle_neq_implies_Rlt a b Hab Hneq).
We prove the intermediate claim H0ltDenR: Rlt 0 den.
An exact proof term for the current goal is (Rlt_0_diff_of_lt a b Hablt).
We prove the intermediate claim HdenPos: 0 < den.
An exact proof term for the current goal is (RltE_lt 0 den H0ltDenR).
We prove the intermediate claim HdenR: den ∈ R.
An exact proof term for the current goal is (real_add_SNo b HbR (minus_SNo a) (real_minus_SNo a HaR)).
We prove the intermediate claim HdenS: SNo den.
An exact proof term for the current goal is (real_SNo den HdenR).
We prove the intermediate claim HtwoR: two ∈ R.
An exact proof term for the current goal is (real_add_SNo 1 real_1 1 real_1).
We prove the intermediate claim HtwoS: SNo two.
An exact proof term for the current goal is (SNo_add_SNo 1 1 SNo_1 SNo_1).
We prove the intermediate claim H0lttwo: 0 < two.
We prove the intermediate claim Htwo2: two = 2.
rewrite the current goal using (add_SNo_1_1_2) (from left to right).
Use reflexivity.
rewrite the current goal using Htwo2 (from left to right).
An exact proof term for the current goal is SNoLt_0_2.
We prove the intermediate claim HabR: ab ∈ R.
An exact proof term for the current goal is (real_add_SNo a HaR b HbR).
We prove the intermediate claim HabS: SNo ab.
An exact proof term for the current goal is (real_SNo ab HabR).
We prove the intermediate claim Hfun: function_on hinv R R.
Let s be given.
Assume HsR: s ∈ R.
We will prove apply_fun hinv s ∈ R.
We prove the intermediate claim HsS: SNo s.
An exact proof term for the current goal is (real_SNo s HsR).
Set num to be the term add_SNo (mul_SNo den s) ab.
We prove the intermediate claim HnumR: num ∈ R.
We prove the intermediate claim HmulR: mul_SNo den s ∈ R.
An exact proof term for the current goal is (real_mul_SNo den HdenR s HsR).
An exact proof term for the current goal is (real_add_SNo (mul_SNo den s) HmulR ab HabR).
We prove the intermediate claim Hhinvdef: hinv = graph R (λs0 : set ⇒ div_SNo (add_SNo (mul_SNo den s0) ab) two).
Use reflexivity.
We prove the intermediate claim Hhs: apply_fun hinv s = div_SNo num two.
rewrite the current goal using Hhinvdef (from left to right).
rewrite the current goal using (apply_fun_graph R (λs0 : set ⇒ div_SNo (add_SNo (mul_SNo den s0) ab) two) s HsR) (from left to right).
Use reflexivity.
rewrite the current goal using Hhs (from left to right).
An exact proof term for the current goal is (real_div_SNo num HnumR two HtwoR).
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 = Tx.
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) at position 2.
Apply (continuous_map_from_subbasis R Tx R S hinv HTx Hfun HS) to the current goal.
Let s be given.
Assume HsS: s ∈ S.
We will prove preimage_of R hinv s ∈ Tx.
We prove the intermediate claim HSdef: S = (({I ∈ 𝒫 R|∃a0 ∈ R, I = open_ray_upper R a0} ∪ {I ∈ 𝒫 R|∃b0 ∈ R, I = open_ray_lower R b0}) ∪ {R}).
Use reflexivity.
We prove the intermediate claim HsS': s ∈ (({I ∈ 𝒫 R|∃a0 ∈ R, I = open_ray_upper R a0} ∪ {I ∈ 𝒫 R|∃b0 ∈ R, I = open_ray_lower R b0}) ∪ {R}).
rewrite the current goal using HSdef (from right to left).
An exact proof term for the current goal is HsS.
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 R hinv s ∈ Tx)) to the current goal.
Assume HsAB: 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 R hinv s ∈ Tx)) to the current goal.
Assume HsUpper: s ∈ {I ∈ 𝒫 R|∃a0 ∈ R, I = open_ray_upper R a0}.
We prove the intermediate claim Hex: ∃c ∈ R, s = open_ray_upper R c.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λI0 : set ⇒ ∃a0 ∈ R, I0 = open_ray_upper R a0) s HsUpper).
Apply Hex to the current goal.
Let c be given.
Assume Hccore.
Apply Hccore to the current goal.
Assume HcR: c ∈ R.
Assume Hseq: s = open_ray_upper R c.
rewrite the current goal using Hseq (from left to right).
Set k to be the term div_SNo (add_SNo (mul_SNo two c) (minus_SNo ab)) den.
We prove the intermediate claim HkR: k ∈ R.
We prove the intermediate claim HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcR).
We prove the intermediate claim HmulR: mul_SNo two c ∈ R.
An exact proof term for the current goal is (real_mul_SNo two HtwoR c HcR).
We prove the intermediate claim HabmR: minus_SNo ab ∈ R.
An exact proof term for the current goal is (real_minus_SNo ab HabR).
We prove the intermediate claim HnumR: add_SNo (mul_SNo two c) (minus_SNo ab) ∈ R.
An exact proof term for the current goal is (real_add_SNo (mul_SNo two c) HmulR (minus_SNo ab) HabmR).
An exact proof term for the current goal is (real_div_SNo (add_SNo (mul_SNo two c) (minus_SNo ab)) HnumR den HdenR).
We prove the intermediate claim HpreEq: preimage_of R hinv (open_ray_upper R c) = open_ray_upper R k.
Set numk to be the term add_SNo (mul_SNo two c) (minus_SNo ab).
We prove the intermediate claim Hkdef: k = div_SNo numk den.
Use reflexivity.
We prove the intermediate claim HnumkS: SNo numk.
We prove the intermediate claim HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcR).
An exact proof term for the current goal is (SNo_add_SNo (mul_SNo two c) (minus_SNo ab) (SNo_mul_SNo two c HtwoS HcS) (SNo_minus_SNo ab HabS)).
Apply set_ext to the current goal.
Let t be given.
Assume Ht: t ∈ preimage_of R hinv (open_ray_upper R c).
We will prove t ∈ open_ray_upper R k.
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (SepE1 R (λx : set ⇒ apply_fun hinv x ∈ open_ray_upper R c) t Ht).
We prove the intermediate claim HhinvRay: apply_fun hinv t ∈ open_ray_upper R c.
An exact proof term for the current goal is (SepE2 R (λx : set ⇒ apply_fun hinv x ∈ open_ray_upper R c) t Ht).
We prove the intermediate claim Hrel: order_rel R c (apply_fun hinv t).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R c x0) (apply_fun hinv t) HhinvRay).
We prove the intermediate claim HltR: Rlt c (apply_fun hinv t).
An exact proof term for the current goal is (order_rel_R_implies_Rlt c (apply_fun hinv t) Hrel).
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 HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcR).
Set numt to be the term add_SNo (mul_SNo den t) ab.
We prove the intermediate claim HnumtR: numt ∈ R.
We prove the intermediate claim HmulR: mul_SNo den t ∈ R.
An exact proof term for the current goal is (real_mul_SNo den HdenR t HtR).
An exact proof term for the current goal is (real_add_SNo (mul_SNo den t) HmulR ab HabR).
We prove the intermediate claim HnumtS: SNo numt.
An exact proof term for the current goal is (real_SNo numt HnumtR).
We prove the intermediate claim Hhinvdef2: hinv = graph R (λs0 : set ⇒ div_SNo (add_SNo (mul_SNo den s0) ab) two).
Use reflexivity.
We prove the intermediate claim Hht: apply_fun hinv t = div_SNo numt two.
rewrite the current goal using Hhinvdef2 (from left to right).
rewrite the current goal using (apply_fun_graph R (λs0 : set ⇒ div_SNo (add_SNo (mul_SNo den s0) ab) two) t HtR) (from left to right).
Use reflexivity.
We prove the intermediate claim HltS: c < apply_fun hinv t.
An exact proof term for the current goal is (RltE_lt c (apply_fun hinv t) HltR).
We prove the intermediate claim HdivLt: c < div_SNo numt two.
rewrite the current goal using Hht (from right to left).
An exact proof term for the current goal is HltS.
We prove the intermediate claim HmulLt: mul_SNo c two < numt.
An exact proof term for the current goal is (div_SNo_pos_LtR' numt two c HnumtS HtwoS HcS H0lttwo HdivLt).
We prove the intermediate claim HmulLt2: mul_SNo two c < numt.
rewrite the current goal using (mul_SNo_com c two HcS HtwoS) (from right to left) at position 1.
An exact proof term for the current goal is HmulLt.
We prove the intermediate claim HsumLt: add_SNo (mul_SNo two c) (minus_SNo ab) < add_SNo numt (minus_SNo ab).
An exact proof term for the current goal is (add_SNo_Lt1 (mul_SNo two c) (minus_SNo ab) numt (SNo_mul_SNo two c HtwoS HcS) (SNo_minus_SNo ab HabS) HnumtS HmulLt2).
We prove the intermediate claim HrightEq: add_SNo numt (minus_SNo ab) = mul_SNo den t.
We prove the intermediate claim Hnumdef: numt = add_SNo (mul_SNo den t) ab.
Use reflexivity.
rewrite the current goal using Hnumdef (from left to right).
An exact proof term for the current goal is (add_SNo_minus_R2 (mul_SNo den t) ab (SNo_mul_SNo den t HdenS HtS) HabS).
We prove the intermediate claim HnumkLt: numk < mul_SNo den t.
rewrite the current goal using HrightEq (from right to left).
An exact proof term for the current goal is HsumLt.
We prove the intermediate claim HnumkLt2: numk < mul_SNo t den.
rewrite the current goal using (mul_SNo_com t den HtS HdenS) (from left to right).
An exact proof term for the current goal is HnumkLt.
We prove the intermediate claim Hklt: k < t.
rewrite the current goal using Hkdef (from left to right).
An exact proof term for the current goal is (div_SNo_pos_LtL numk den t HnumkS HdenS HtS HdenPos HnumkLt2).
We prove the intermediate claim HkltR: Rlt k t.
An exact proof term for the current goal is (RltI k t HkR HtR Hklt).
We prove the intermediate claim Hrelkt: order_rel R k t.
An exact proof term for the current goal is (Rlt_implies_order_rel_R k t HkltR).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R k x0) t HtR Hrelkt).
Let t be given.
Assume Ht: t ∈ open_ray_upper R k.
We will prove t ∈ preimage_of R hinv (open_ray_upper R c).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ order_rel R k x0) t Ht).
We prove the intermediate claim Hrelkt: order_rel R k t.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R k x0) t Ht).
We prove the intermediate claim HltR: Rlt k t.
An exact proof term for the current goal is (order_rel_R_implies_Rlt k t Hrelkt).
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 HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcR).
We prove the intermediate claim HltS: k < t.
An exact proof term for the current goal is (RltE_lt k t HltR).
We prove the intermediate claim HkS: SNo k.
An exact proof term for the current goal is (real_SNo k HkR).
We prove the intermediate claim HltS': div_SNo numk den < t.
rewrite the current goal using Hkdef (from right to left) at position 1.
An exact proof term for the current goal is HltS.
We prove the intermediate claim HnumkLt: numk < mul_SNo t den.
An exact proof term for the current goal is (div_SNo_pos_LtL' numk den t HnumkS HdenS HtS HdenPos HltS').
We prove the intermediate claim HnumkLt2: numk < mul_SNo den t.
rewrite the current goal using (mul_SNo_com t den HtS HdenS) (from right to left).
An exact proof term for the current goal is HnumkLt.
We prove the intermediate claim HsumLt: add_SNo numk ab < add_SNo (mul_SNo den t) ab.
An exact proof term for the current goal is (add_SNo_Lt1 numk ab (mul_SNo den t) HnumkS HabS (SNo_mul_SNo den t HdenS HtS) HnumkLt2).
We prove the intermediate claim HnumkEq: add_SNo numk ab = mul_SNo two c.
We prove the intermediate claim Hnumkdef2: numk = add_SNo (mul_SNo two c) (minus_SNo ab).
Use reflexivity.
rewrite the current goal using Hnumkdef2 (from left to right).
An exact proof term for the current goal is (add_SNo_minus_R2' (mul_SNo two c) ab (SNo_mul_SNo two c HtwoS HcS) HabS).
We prove the intermediate claim HnumtLt: mul_SNo two c < add_SNo (mul_SNo den t) ab.
rewrite the current goal using HnumkEq (from right to left) at position 1.
An exact proof term for the current goal is HsumLt.
We prove the intermediate claim HnumtLt2: mul_SNo c two < add_SNo (mul_SNo den t) ab.
rewrite the current goal using (mul_SNo_com c two HcS HtwoS) (from left to right).
An exact proof term for the current goal is HnumtLt.
Set numt to be the term add_SNo (mul_SNo den t) ab.
We prove the intermediate claim HnumtR: numt ∈ R.
We prove the intermediate claim HmulR: mul_SNo den t ∈ R.
An exact proof term for the current goal is (real_mul_SNo den HdenR t HtR).
An exact proof term for the current goal is (real_add_SNo (mul_SNo den t) HmulR ab HabR).
We prove the intermediate claim HnumtS: SNo numt.
An exact proof term for the current goal is (real_SNo numt HnumtR).
We prove the intermediate claim HdivLt: c < div_SNo numt two.
An exact proof term for the current goal is (div_SNo_pos_LtR numt two c HnumtS HtwoS HcS H0lttwo HnumtLt2).
We prove the intermediate claim Hhinvdef2: hinv = graph R (λs0 : set ⇒ div_SNo (add_SNo (mul_SNo den s0) ab) two).
Use reflexivity.
We prove the intermediate claim Hht: apply_fun hinv t = div_SNo numt two.
rewrite the current goal using Hhinvdef2 (from left to right).
rewrite the current goal using (apply_fun_graph R (λs0 : set ⇒ div_SNo (add_SNo (mul_SNo den s0) ab) two) t HtR) (from left to right).
Use reflexivity.
We prove the intermediate claim HltS2: c < apply_fun hinv t.
rewrite the current goal using Hht (from left to right).
An exact proof term for the current goal is HdivLt.
We prove the intermediate claim HhinvRt: apply_fun hinv t ∈ R.
An exact proof term for the current goal is (Hfun t HtR).
We prove the intermediate claim HltR2: Rlt c (apply_fun hinv t).
An exact proof term for the current goal is (RltI c (apply_fun hinv t) HcR HhinvRt HltS2).
We prove the intermediate claim Hrelct: order_rel R c (apply_fun hinv t).
An exact proof term for the current goal is (Rlt_implies_order_rel_R c (apply_fun hinv t) HltR2).
We prove the intermediate claim Hray: apply_fun hinv t ∈ open_ray_upper R c.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R c x0) (apply_fun hinv t) HhinvRt Hrelct).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ apply_fun hinv x0 ∈ open_ray_upper R c) t HtR Hray).
rewrite the current goal using HpreEq (from left to right).
rewrite the current goal using standard_topology_is_order_topology (from right to left).
We prove the intermediate claim HsRay: open_ray_upper R k ∈ open_rays_subbasis R.
An exact proof term for the current goal is (open_ray_upper_in_open_rays_subbasis R k HkR).
An exact proof term for the current goal is (open_rays_subbasis_sub_order_topology_R (open_ray_upper R k) HsRay).
Assume HsLower: s ∈ {I ∈ 𝒫 R|∃b0 ∈ R, I = open_ray_lower R b0}.
We prove the intermediate claim Hex: ∃c ∈ R, s = open_ray_lower R c.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λI0 : set ⇒ ∃b0 ∈ R, I0 = open_ray_lower R b0) s HsLower).
Apply Hex to the current goal.
Let c be given.
Assume Hccore.
Apply Hccore to the current goal.
Assume HcR: c ∈ R.
Assume Hseq: s = open_ray_lower R c.
rewrite the current goal using Hseq (from left to right).
Set k to be the term div_SNo (add_SNo (mul_SNo two c) (minus_SNo ab)) den.
We prove the intermediate claim HkR: k ∈ R.
We prove the intermediate claim HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcR).
We prove the intermediate claim HmulR: mul_SNo two c ∈ R.
An exact proof term for the current goal is (real_mul_SNo two HtwoR c HcR).
We prove the intermediate claim HabmR: minus_SNo ab ∈ R.
An exact proof term for the current goal is (real_minus_SNo ab HabR).
We prove the intermediate claim HnumR: add_SNo (mul_SNo two c) (minus_SNo ab) ∈ R.
An exact proof term for the current goal is (real_add_SNo (mul_SNo two c) HmulR (minus_SNo ab) HabmR).
An exact proof term for the current goal is (real_div_SNo (add_SNo (mul_SNo two c) (minus_SNo ab)) HnumR den HdenR).
We prove the intermediate claim HpreEq: preimage_of R hinv (open_ray_lower R c) = open_ray_lower R k.
Set numk to be the term add_SNo (mul_SNo two c) (minus_SNo ab).
We prove the intermediate claim Hkdef: k = div_SNo numk den.
Use reflexivity.
We prove the intermediate claim HnumkS: SNo numk.
We prove the intermediate claim HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcR).
An exact proof term for the current goal is (SNo_add_SNo (mul_SNo two c) (minus_SNo ab) (SNo_mul_SNo two c HtwoS HcS) (SNo_minus_SNo ab HabS)).
Apply set_ext to the current goal.
Let t be given.
Assume Ht: t ∈ preimage_of R hinv (open_ray_lower R c).
We will prove t ∈ open_ray_lower R k.
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (SepE1 R (λx : set ⇒ apply_fun hinv x ∈ open_ray_lower R c) t Ht).
We prove the intermediate claim HhinvRay: apply_fun hinv t ∈ open_ray_lower R c.
An exact proof term for the current goal is (SepE2 R (λx : set ⇒ apply_fun hinv x ∈ open_ray_lower R c) t Ht).
We prove the intermediate claim Hrel: order_rel R (apply_fun hinv t) c.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R x0 c) (apply_fun hinv t) HhinvRay).
We prove the intermediate claim HltR: Rlt (apply_fun hinv t) c.
An exact proof term for the current goal is (order_rel_R_implies_Rlt (apply_fun hinv t) c Hrel).
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 HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcR).
Set numt to be the term add_SNo (mul_SNo den t) ab.
We prove the intermediate claim HnumtR: numt ∈ R.
We prove the intermediate claim HmulR: mul_SNo den t ∈ R.
An exact proof term for the current goal is (real_mul_SNo den HdenR t HtR).
An exact proof term for the current goal is (real_add_SNo (mul_SNo den t) HmulR ab HabR).
We prove the intermediate claim HnumtS: SNo numt.
An exact proof term for the current goal is (real_SNo numt HnumtR).
We prove the intermediate claim Hhinvdef2: hinv = graph R (λs0 : set ⇒ div_SNo (add_SNo (mul_SNo den s0) ab) two).
Use reflexivity.
We prove the intermediate claim Hht: apply_fun hinv t = div_SNo numt two.
rewrite the current goal using Hhinvdef2 (from left to right).
rewrite the current goal using (apply_fun_graph R (λs0 : set ⇒ div_SNo (add_SNo (mul_SNo den s0) ab) two) t HtR) (from left to right).
Use reflexivity.
We prove the intermediate claim HltS: apply_fun hinv t < c.
An exact proof term for the current goal is (RltE_lt (apply_fun hinv t) c HltR).
We prove the intermediate claim HdivLt: div_SNo numt two < c.
rewrite the current goal using Hht (from right to left).
An exact proof term for the current goal is HltS.
We prove the intermediate claim HmulLt: numt < mul_SNo c two.
An exact proof term for the current goal is (div_SNo_pos_LtL' numt two c HnumtS HtwoS HcS H0lttwo HdivLt).
We prove the intermediate claim HmulLt2: numt < mul_SNo two c.
rewrite the current goal using (mul_SNo_com c two HcS HtwoS) (from right to left).
An exact proof term for the current goal is HmulLt.
We prove the intermediate claim HsumLt: add_SNo numt (minus_SNo ab) < add_SNo (mul_SNo two c) (minus_SNo ab).
An exact proof term for the current goal is (add_SNo_Lt1 numt (minus_SNo ab) (mul_SNo two c) HnumtS (SNo_minus_SNo ab HabS) (SNo_mul_SNo two c HtwoS HcS) HmulLt2).
We prove the intermediate claim HleftEq: add_SNo numt (minus_SNo ab) = mul_SNo den t.
We prove the intermediate claim Hnumdef: numt = add_SNo (mul_SNo den t) ab.
Use reflexivity.
rewrite the current goal using Hnumdef (from left to right).
An exact proof term for the current goal is (add_SNo_minus_R2 (mul_SNo den t) ab (SNo_mul_SNo den t HdenS HtS) HabS).
We prove the intermediate claim HdtLt: mul_SNo den t < numk.
rewrite the current goal using HleftEq (from right to left) at position 1.
An exact proof term for the current goal is HsumLt.
We prove the intermediate claim HdtLt2: mul_SNo t den < numk.
rewrite the current goal using (mul_SNo_com t den HtS HdenS) (from left to right).
An exact proof term for the current goal is HdtLt.
We prove the intermediate claim Htlt: t < div_SNo numk den.
An exact proof term for the current goal is (div_SNo_pos_LtR numk den t HnumkS HdenS HtS HdenPos HdtLt2).
We prove the intermediate claim Htlt2: t < k.
rewrite the current goal using Hkdef (from left to right).
An exact proof term for the current goal is Htlt.
We prove the intermediate claim HtltR: Rlt t k.
An exact proof term for the current goal is (RltI t k HtR HkR Htlt2).
We prove the intermediate claim Hreltk: order_rel R t k.
An exact proof term for the current goal is (Rlt_implies_order_rel_R t k HtltR).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R x0 k) t HtR Hreltk).
Let t be given.
Assume Ht: t ∈ open_ray_lower R k.
We will prove t ∈ preimage_of R hinv (open_ray_lower R c).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ order_rel R x0 k) t Ht).
We prove the intermediate claim Hreltk: order_rel R t k.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R x0 k) t Ht).
We prove the intermediate claim HltR: Rlt t k.
An exact proof term for the current goal is (order_rel_R_implies_Rlt t k Hreltk).
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 HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcR).
We prove the intermediate claim HltS: t < k.
An exact proof term for the current goal is (RltE_lt t k HltR).
We prove the intermediate claim HkS: SNo k.
An exact proof term for the current goal is (real_SNo k HkR).
We prove the intermediate claim HltS': t < div_SNo numk den.
rewrite the current goal using Hkdef (from right to left).
An exact proof term for the current goal is HltS.
We prove the intermediate claim HdtLt: mul_SNo t den < numk.
An exact proof term for the current goal is (div_SNo_pos_LtR' numk den t HnumkS HdenS HtS HdenPos HltS').
We prove the intermediate claim HdtLt2: mul_SNo den t < numk.
rewrite the current goal using (mul_SNo_com t den HtS HdenS) (from right to left) at position 1.
An exact proof term for the current goal is HdtLt.
We prove the intermediate claim HsumLt: add_SNo (mul_SNo den t) ab < add_SNo numk ab.
An exact proof term for the current goal is (add_SNo_Lt1 (mul_SNo den t) ab numk (SNo_mul_SNo den t HdenS HtS) HabS HnumkS HdtLt2).
We prove the intermediate claim HnumkEq: add_SNo numk ab = mul_SNo two c.
We prove the intermediate claim Hnumkdef2: numk = add_SNo (mul_SNo two c) (minus_SNo ab).
Use reflexivity.
rewrite the current goal using Hnumkdef2 (from left to right).
An exact proof term for the current goal is (add_SNo_minus_R2' (mul_SNo two c) ab (SNo_mul_SNo two c HtwoS HcS) HabS).
We prove the intermediate claim HnumtLt: add_SNo (mul_SNo den t) ab < mul_SNo two c.
rewrite the current goal using HnumkEq (from right to left).
An exact proof term for the current goal is HsumLt.
We prove the intermediate claim HnumtLt2: add_SNo (mul_SNo den t) ab < mul_SNo c two.
rewrite the current goal using (mul_SNo_com c two HcS HtwoS) (from left to right).
An exact proof term for the current goal is HnumtLt.
Set numt to be the term add_SNo (mul_SNo den t) ab.
We prove the intermediate claim HnumtR: numt ∈ R.
We prove the intermediate claim HmulR: mul_SNo den t ∈ R.
An exact proof term for the current goal is (real_mul_SNo den HdenR t HtR).
An exact proof term for the current goal is (real_add_SNo (mul_SNo den t) HmulR ab HabR).
We prove the intermediate claim HnumtS: SNo numt.
An exact proof term for the current goal is (real_SNo numt HnumtR).
We prove the intermediate claim HdivLt: div_SNo numt two < c.
An exact proof term for the current goal is (div_SNo_pos_LtL numt two c HnumtS HtwoS HcS H0lttwo HnumtLt2).
We prove the intermediate claim Hhinvdef2: hinv = graph R (λs0 : set ⇒ div_SNo (add_SNo (mul_SNo den s0) ab) two).
Use reflexivity.
We prove the intermediate claim Hht: apply_fun hinv t = div_SNo numt two.
rewrite the current goal using Hhinvdef2 (from left to right).
rewrite the current goal using (apply_fun_graph R (λs0 : set ⇒ div_SNo (add_SNo (mul_SNo den s0) ab) two) t HtR) (from left to right).
Use reflexivity.
We prove the intermediate claim HltS2: apply_fun hinv t < c.
rewrite the current goal using Hht (from left to right).
An exact proof term for the current goal is HdivLt.
We prove the intermediate claim HhinvRt: apply_fun hinv t ∈ R.
An exact proof term for the current goal is (Hfun t HtR).
We prove the intermediate claim HltR2: Rlt (apply_fun hinv t) c.
An exact proof term for the current goal is (RltI (apply_fun hinv t) c HhinvRt HcR HltS2).
We prove the intermediate claim Hrelct: order_rel R (apply_fun hinv t) c.
An exact proof term for the current goal is (Rlt_implies_order_rel_R (apply_fun hinv t) c HltR2).
We prove the intermediate claim Hray: apply_fun hinv t ∈ open_ray_lower R c.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R x0 c) (apply_fun hinv t) HhinvRt Hrelct).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ apply_fun hinv x0 ∈ open_ray_lower R c) t HtR Hray).
rewrite the current goal using HpreEq (from left to right).
rewrite the current goal using standard_topology_is_order_topology (from right to left).
We prove the intermediate claim HsRay: open_ray_lower R k ∈ open_rays_subbasis R.
An exact proof term for the current goal is (open_ray_lower_in_open_rays_subbasis R k HkR).
An exact proof term for the current goal is (open_rays_subbasis_sub_order_topology_R (open_ray_lower R k) HsRay).
An exact proof term for the current goal is HsAB.
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).
rewrite the current goal using (preimage_of_whole R R hinv Hfun) (from left to right).
An exact proof term for the current goal is (topology_has_X R Tx HTx).
An exact proof term for the current goal is HsS'.
We prove the intermediate claim HhinvDom: continuous_map Im1 (subspace_topology R R_standard_topology Im1) R R_standard_topology hinv.
An exact proof term for the current goal is (continuous_on_subspace_rule R R_standard_topology R R_standard_topology hinv Im1 HTstd HTstd HIm1Sub HhinvR).
We prove the intermediate claim HhinvImg: ∀s : set, s ∈ Im1 → apply_fun hinv s ∈ Iab.
Let s be given.
Assume HsI: s ∈ Im1.
We will prove apply_fun hinv s ∈ Iab.
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (RleE_left a b Hab).
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is (RleE_right a b Hab).
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 HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
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 HsR: s ∈ R.
An exact proof term for the current goal is (HIm1Sub s HsI).
We prove the intermediate claim HsS: SNo s.
An exact proof term for the current goal is (real_SNo s HsR).
We prove the intermediate claim Hsbounds: Rle (minus_SNo 1) s ∧ Rle s 1.
An exact proof term for the current goal is (closed_interval_bounds (minus_SNo 1) 1 s Hm1R real_1 HsI).
We prove the intermediate claim Hm1leS: Rle (minus_SNo 1) s.
An exact proof term for the current goal is (andEL (Rle (minus_SNo 1) s) (Rle s 1) Hsbounds).
We prove the intermediate claim Hsle1: Rle s 1.
An exact proof term for the current goal is (andER (Rle (minus_SNo 1) s) (Rle s 1) Hsbounds).
Set den to be the term add_SNo b (minus_SNo a).
Set two to be the term add_SNo 1 1.
Set ab to be the term add_SNo a b.
Set num to be the term add_SNo (mul_SNo den s) ab.
We prove the intermediate claim Hablt: Rlt a b.
An exact proof term for the current goal is (Rle_neq_implies_Rlt a b Hab Hneq).
We prove the intermediate claim H0ltDenR: Rlt 0 den.
An exact proof term for the current goal is (Rlt_0_diff_of_lt a b Hablt).
We prove the intermediate claim HdenPos: 0 < den.
An exact proof term for the current goal is (RltE_lt 0 den H0ltDenR).
We prove the intermediate claim HdenR: den ∈ R.
An exact proof term for the current goal is (real_add_SNo b HbR (minus_SNo a) (real_minus_SNo a HaR)).
We prove the intermediate claim HdenS: SNo den.
An exact proof term for the current goal is (real_SNo den HdenR).
We prove the intermediate claim Hden_ne0: den ≠ 0.
Assume Hden0: den = 0.
We prove the intermediate claim H0lt0S: 0 < 0.
rewrite the current goal using Hden0 (from right to left) at position 2.
An exact proof term for the current goal is (RltE_lt 0 den H0ltDenR).
We prove the intermediate claim H0lt0R: Rlt 0 0.
An exact proof term for the current goal is (RltI 0 0 real_0 real_0 H0lt0S).
An exact proof term for the current goal is ((not_Rlt_refl 0 real_0) H0lt0R).
We prove the intermediate claim HtwoS: SNo two.
An exact proof term for the current goal is (SNo_add_SNo 1 1 SNo_1 SNo_1).
We prove the intermediate claim H0lttwo: 0 < two.
We prove the intermediate claim Htwo2: two = 2.
rewrite the current goal using (add_SNo_1_1_2) (from left to right).
Use reflexivity.
rewrite the current goal using Htwo2 (from left to right).
An exact proof term for the current goal is SNoLt_0_2.
We prove the intermediate claim Htwo_ne0: two ≠ 0.
Assume Htwo0: two = 0.
We prove the intermediate claim Htwo2: two = 2.
rewrite the current goal using (add_SNo_1_1_2) (from left to right).
Use reflexivity.
We prove the intermediate claim H20: 2 = 0.
rewrite the current goal using Htwo2 (from right to left) at position 1.
An exact proof term for the current goal is Htwo0.
An exact proof term for the current goal is (neq_2_0 H20).
We prove the intermediate claim HabR: ab ∈ R.
An exact proof term for the current goal is (real_add_SNo a HaR b HbR).
We prove the intermediate claim HabS: SNo ab.
An exact proof term for the current goal is (real_SNo ab HabR).
We prove the intermediate claim HnumR: num ∈ R.
We prove the intermediate claim HmulR: mul_SNo den s ∈ R.
An exact proof term for the current goal is (real_mul_SNo den HdenR s HsR).
An exact proof term for the current goal is (real_add_SNo (mul_SNo den s) HmulR ab HabR).
We prove the intermediate claim HnumS: SNo num.
An exact proof term for the current goal is (real_SNo num HnumR).
We prove the intermediate claim Hhinvdef: hinv = graph R (λs0 : set ⇒ div_SNo (add_SNo (mul_SNo (add_SNo b (minus_SNo a)) s0) (add_SNo a b)) (add_SNo 1 1)).
Use reflexivity.
We prove the intermediate claim Hhinvs: apply_fun hinv s = div_SNo num two.
rewrite the current goal using Hhinvdef (from left to right).
rewrite the current goal using (apply_fun_graph R (λs0 : set ⇒ div_SNo (add_SNo (mul_SNo (add_SNo b (minus_SNo a)) s0) (add_SNo a b)) (add_SNo 1 1)) s HsR) (from left to right).
Use reflexivity.
We prove the intermediate claim HhinvsR: apply_fun hinv s ∈ R.
rewrite the current goal using Hhinvs (from left to right).
An exact proof term for the current goal is (real_div_SNo num HnumR two (real_add_SNo 1 real_1 1 real_1)).
We prove the intermediate claim Hlo: Rle a (apply_fun hinv s).
Apply (RleI a (apply_fun hinv s) HaR HhinvsR) to the current goal.
Assume Hlt: Rlt (apply_fun hinv s) a.
We prove the intermediate claim HltS: apply_fun hinv s < a.
An exact proof term for the current goal is (RltE_lt (apply_fun hinv s) a Hlt).
We prove the intermediate claim HdivLt: div_SNo num two < a.
rewrite the current goal using Hhinvs (from right to left).
An exact proof term for the current goal is HltS.
We prove the intermediate claim HnumLt: num < mul_SNo a two.
An exact proof term for the current goal is (div_SNo_pos_LtL' num two a HnumS HtwoS HaS H0lttwo HdivLt).
We prove the intermediate claim Hm1denEq: mul_SNo (minus_SNo 1) den = add_SNo a (minus_SNo b).
We prove the intermediate claim Hm1S: SNo (minus_SNo 1).
An exact proof term for the current goal is (SNo_minus_SNo 1 SNo_1).
We prove the intermediate claim Hm1den: mul_SNo (minus_SNo 1) den = minus_SNo den.
We prove the intermediate claim Hcomm: mul_SNo (minus_SNo 1) den = mul_SNo den (minus_SNo 1).
An exact proof term for the current goal is (mul_SNo_com (minus_SNo 1) den Hm1S HdenS).
rewrite the current goal using Hcomm (from left to right).
rewrite the current goal using (mul_SNo_minus_distrR den 1 HdenS SNo_1) (from left to right).
rewrite the current goal using (mul_SNo_oneR den HdenS) (from left to right).
Use reflexivity.
rewrite the current goal using Hm1den (from left to right).
rewrite the current goal using (minus_add_SNo_distr b (minus_SNo a) HbS (SNo_minus_SNo a HaS)) (from left to right).
rewrite the current goal using (minus_SNo_minus_SNo_real a HaR) (from left to right).
We prove the intermediate claim Hcom: add_SNo (minus_SNo b) a = add_SNo a (minus_SNo b).
An exact proof term for the current goal is (add_SNo_com (minus_SNo b) a (SNo_minus_SNo b HbS) HaS).
rewrite the current goal using Hcom (from left to right).
Use reflexivity.
We prove the intermediate claim H2aEq: mul_SNo a two = add_SNo (add_SNo a (minus_SNo b)) ab.
We prove the intermediate claim Habdef: ab = add_SNo a b.
Use reflexivity.
rewrite the current goal using Habdef (from left to right).
rewrite the current goal using (mul_SNo_com a two HaS HtwoS) (from left to right).
We prove the intermediate claim Hmul2a: mul_SNo two a = add_SNo a a.
We prove the intermediate claim HtwoDef: two = add_SNo 1 1.
Use reflexivity.
rewrite the current goal using HtwoDef (from left to right).
rewrite the current goal using (mul_SNo_distrR 1 1 a SNo_1 SNo_1 HaS) (from left to right).
rewrite the current goal using (mul_SNo_oneL a HaS) (from left to right) at position 1.
rewrite the current goal using (mul_SNo_oneL a HaS) (from left to right).
Use reflexivity.
rewrite the current goal using Hmul2a (from left to right).
rewrite the current goal using (add_SNo_assoc (add_SNo a (minus_SNo b)) a b (SNo_add_SNo a (minus_SNo b) HaS (SNo_minus_SNo b HbS)) HaS HbS) (from left to right).
rewrite the current goal using (add_SNo_com_3b_1_2 a (minus_SNo b) a HaS (SNo_minus_SNo b HbS) HaS) (from left to right) at position 1.
rewrite the current goal using (add_SNo_assoc (add_SNo a a) (minus_SNo b) b (SNo_add_SNo a a HaS HaS) (SNo_minus_SNo b HbS) HbS) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_linv b HbS) (from left to right).
rewrite the current goal using (add_SNo_0R (add_SNo a a) (SNo_add_SNo a a HaS HaS)) (from left to right).
Use reflexivity.
We prove the intermediate claim HrhsS: SNo (add_SNo a (minus_SNo b)).
An exact proof term for the current goal is (SNo_add_SNo a (minus_SNo b) HaS (SNo_minus_SNo b HbS)).
We prove the intermediate claim HmulLt: num < add_SNo (add_SNo a (minus_SNo b)) ab.
rewrite the current goal using H2aEq (from right to left) at position 1.
An exact proof term for the current goal is HnumLt.
We prove the intermediate claim Hnumdef: num = add_SNo (mul_SNo den s) ab.
Use reflexivity.
We prove the intermediate claim HmulLt': add_SNo (mul_SNo den s) ab < add_SNo (add_SNo a (minus_SNo b)) ab.
rewrite the current goal using Hnumdef (from left to right) at position 1.
An exact proof term for the current goal is HmulLt.
We prove the intermediate claim Hcancel: mul_SNo den s < add_SNo a (minus_SNo b).
An exact proof term for the current goal is (add_SNo_Lt1_cancel (mul_SNo den s) ab (add_SNo a (minus_SNo b)) (SNo_mul_SNo den s HdenS HsS) HabS HrhsS HmulLt').
We prove the intermediate claim Hm1S: SNo (minus_SNo 1).
An exact proof term for the current goal is (SNo_minus_SNo 1 SNo_1).
We prove the intermediate claim HsdLt: mul_SNo den s < mul_SNo (minus_SNo 1) den.
rewrite the current goal using Hm1denEq (from left to right) at position 1.
An exact proof term for the current goal is Hcancel.
We prove the intermediate claim HsLt: div_SNo (mul_SNo den s) den < minus_SNo 1.
An exact proof term for the current goal is (div_SNo_pos_LtL (mul_SNo den s) den (minus_SNo 1) (SNo_mul_SNo den s HdenS HsS) HdenS Hm1S HdenPos HsdLt).
We prove the intermediate claim HdivEq: div_SNo (mul_SNo den s) den = s.
We prove the intermediate claim HmulId: mul_SNo den s = mul_SNo den s.
Use reflexivity.
An exact proof term for the current goal is (mul_div_SNo_nonzero_eq (mul_SNo den s) den s (SNo_mul_SNo den s HdenS HsS) HdenS HsS Hden_ne0 HmulId).
We prove the intermediate claim HsLtS: s < minus_SNo 1.
rewrite the current goal using HdivEq (from right to left) at position 1.
An exact proof term for the current goal is HsLt.
We prove the intermediate claim HsLtR: Rlt s (minus_SNo 1).
An exact proof term for the current goal is (RltI s (minus_SNo 1) HsR Hm1R HsLtS).
An exact proof term for the current goal is ((RleE_nlt (minus_SNo 1) s Hm1leS) HsLtR).
We prove the intermediate claim Hhi: Rle (apply_fun hinv s) b.
Apply (RleI (apply_fun hinv s) b HhinvsR HbR) to the current goal.
Assume Hlt: Rlt b (apply_fun hinv s).
We prove the intermediate claim HltS: b < apply_fun hinv s.
An exact proof term for the current goal is (RltE_lt b (apply_fun hinv s) Hlt).
We prove the intermediate claim HdivLt: b < div_SNo num two.
rewrite the current goal using Hhinvs (from right to left).
An exact proof term for the current goal is HltS.
We prove the intermediate claim HnumGt: mul_SNo b two < num.
An exact proof term for the current goal is (div_SNo_pos_LtR' num two b HnumS HtwoS HbS H0lttwo HdivLt).
We prove the intermediate claim Hm1S: SNo (minus_SNo 1).
An exact proof term for the current goal is (SNo_minus_SNo 1 SNo_1).
We prove the intermediate claim Hb2Eq: mul_SNo b two = add_SNo den ab.
We prove the intermediate claim Habdef: ab = add_SNo a b.
Use reflexivity.
We prove the intermediate claim Hdendef: den = add_SNo b (minus_SNo a).
Use reflexivity.
rewrite the current goal using Habdef (from left to right).
rewrite the current goal using Hdendef (from left to right).
We prove the intermediate claim Hmul2b: mul_SNo two b = add_SNo b b.
We prove the intermediate claim HtwoDef: two = add_SNo 1 1.
Use reflexivity.
rewrite the current goal using HtwoDef (from left to right).
rewrite the current goal using (mul_SNo_distrR 1 1 b SNo_1 SNo_1 HbS) (from left to right).
rewrite the current goal using (mul_SNo_oneL b HbS) (from left to right) at position 1.
rewrite the current goal using (mul_SNo_oneL b HbS) (from left to right).
Use reflexivity.
rewrite the current goal using (mul_SNo_com b two HbS HtwoS) (from left to right).
rewrite the current goal using Hmul2b (from left to right).
rewrite the current goal using (add_SNo_assoc (add_SNo b (minus_SNo a)) a b (SNo_add_SNo b (minus_SNo a) HbS (SNo_minus_SNo a HaS)) HaS HbS) (from left to right).
rewrite the current goal using (add_SNo_com_3b_1_2 b (minus_SNo a) a HbS (SNo_minus_SNo a HaS) HaS) (from left to right) at position 1.
rewrite the current goal using (add_SNo_minus_R2 b a HbS HaS) (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim Hnumdef: num = add_SNo (mul_SNo den s) ab.
Use reflexivity.
We prove the intermediate claim HrhsLt: add_SNo den ab < add_SNo (mul_SNo den s) ab.
rewrite the current goal using Hb2Eq (from right to left) at position 1.
rewrite the current goal using Hnumdef (from right to left) at position 1.
An exact proof term for the current goal is HnumGt.
We prove the intermediate claim HdenLt: den < mul_SNo den s.
An exact proof term for the current goal is (add_SNo_Lt1_cancel den ab (mul_SNo den s) HdenS HabS (SNo_mul_SNo den s HdenS HsS) HrhsLt).
We prove the intermediate claim HoneDenLt: mul_SNo 1 den < mul_SNo den s.
rewrite the current goal using (mul_SNo_oneL den HdenS) (from left to right) at position 1.
An exact proof term for the current goal is HdenLt.
We prove the intermediate claim HsGt: 1 < div_SNo (mul_SNo den s) den.
An exact proof term for the current goal is (div_SNo_pos_LtR (mul_SNo den s) den 1 (SNo_mul_SNo den s HdenS HsS) HdenS SNo_1 HdenPos HoneDenLt).
We prove the intermediate claim HdivEq: div_SNo (mul_SNo den s) den = s.
We prove the intermediate claim HmulId: mul_SNo den s = mul_SNo den s.
Use reflexivity.
An exact proof term for the current goal is (mul_div_SNo_nonzero_eq (mul_SNo den s) den s (SNo_mul_SNo den s HdenS HsS) HdenS HsS Hden_ne0 HmulId).
We prove the intermediate claim H1LtS: 1 < s.
rewrite the current goal using HdivEq (from right to left) at position 1.
An exact proof term for the current goal is HsGt.
We prove the intermediate claim H1LtSR: Rlt 1 s.
An exact proof term for the current goal is (RltI 1 s real_1 HsR H1LtS).
An exact proof term for the current goal is ((RleE_nlt s 1 Hsle1) H1LtSR).
An exact proof term for the current goal is (closed_intervalI_of_Rle a b (apply_fun hinv s) HaR HbR HhinvsR Hlo Hhi).
We prove the intermediate claim HhinvCod: continuous_map Im1 (subspace_topology R R_standard_topology Im1) Iab (subspace_topology R R_standard_topology Iab) hinv.
An exact proof term for the current goal is (continuous_map_range_restrict Im1 (subspace_topology R R_standard_topology Im1) R R_standard_topology hinv Iab HhinvDom HIabSub HhinvImg).
We prove the intermediate claim HTiabEq: closed_interval_topology a b = subspace_topology R R_standard_topology Iab.
Use reflexivity.
We prove the intermediate claim HTim1Eq: closed_interval_topology (minus_SNo 1) 1 = subspace_topology R R_standard_topology Im1.
Use reflexivity.
rewrite the current goal using HTim1Eq (from left to right).
rewrite the current goal using HTiabEq (from left to right).
An exact proof term for the current goal is HhinvCod.
Apply andI to the current goal.
Let t be given.
Assume Ht: t ∈ closed_interval a b.
We will prove apply_fun hinv (apply_fun h t) = t.
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (RleE_left a b Hab).
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is (RleE_right a b Hab).
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 HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim HsubI: closed_interval a b ⊆ R.
An exact proof term for the current goal is (closed_interval_sub_R a b).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (HsubI t Ht).
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
Set den to be the term add_SNo b (minus_SNo a).
Set two to be the term add_SNo 1 1.
Set ab to be the term add_SNo a b.
Set num to be the term add_SNo (mul_SNo two t) (minus_SNo ab).
We prove the intermediate claim HabR: ab ∈ R.
An exact proof term for the current goal is (real_add_SNo a HaR b HbR).
We prove the intermediate claim HabS: SNo ab.
An exact proof term for the current goal is (real_SNo ab HabR).
We prove the intermediate claim HdenR: den ∈ R.
An exact proof term for the current goal is (real_add_SNo b HbR (minus_SNo a) (real_minus_SNo a HaR)).
We prove the intermediate claim HdenS: SNo den.
An exact proof term for the current goal is (real_SNo den HdenR).
We prove the intermediate claim HtwoS: SNo two.
An exact proof term for the current goal is (SNo_add_SNo 1 1 SNo_1 SNo_1).
We prove the intermediate claim Htwo_ne0: two ≠ 0.
Assume Htwo0: two = 0.
We prove the intermediate claim Htwo2: two = 2.
rewrite the current goal using (add_SNo_1_1_2) (from left to right).
Use reflexivity.
We prove the intermediate claim H20: 2 = 0.
rewrite the current goal using Htwo2 (from right to left) at position 1.
An exact proof term for the current goal is Htwo0.
An exact proof term for the current goal is (neq_2_0 H20).
We prove the intermediate claim Hden_ne0: den ≠ 0.
Assume Hden0: den = 0.
We prove the intermediate claim Hmab: minus_SNo a ∈ R.
An exact proof term for the current goal is (real_minus_SNo a HaR).
We prove the intermediate claim HmabS: SNo (minus_SNo a).
An exact proof term for the current goal is (real_SNo (minus_SNo a) Hmab).
We prove the intermediate claim Hlhs0: add_SNo b (minus_SNo a) = add_SNo a (minus_SNo a).
rewrite the current goal using Hden0 (from left to right) at position 1.
rewrite the current goal using (add_SNo_minus_SNo_rinv a HaS) (from left to right).
Use reflexivity.
We prove the intermediate claim Hba: b = a.
An exact proof term for the current goal is (add_SNo_cancel_R b (minus_SNo a) a HbS HmabS HaS Hlhs0).
We prove the intermediate claim Habeq: a = b.
rewrite the current goal using Hba (from right to left).
Use reflexivity.
An exact proof term for the current goal is (Hneq Habeq).
We prove the intermediate claim HnumR: num ∈ R.
We prove the intermediate claim HtwoR: two ∈ R.
An exact proof term for the current goal is (real_add_SNo 1 real_1 1 real_1).
We prove the intermediate claim HmulR: mul_SNo two t ∈ R.
An exact proof term for the current goal is (real_mul_SNo two HtwoR t HtR).
We prove the intermediate claim HabmR: minus_SNo ab ∈ R.
An exact proof term for the current goal is (real_minus_SNo ab HabR).
An exact proof term for the current goal is (real_add_SNo (mul_SNo two t) HmulR (minus_SNo ab) HabmR).
We prove the intermediate claim HnumS: SNo num.
An exact proof term for the current goal is (real_SNo num HnumR).
We prove the intermediate claim Hhdef: h = graph R (λt0 : set ⇒ div_SNo (add_SNo (mul_SNo (add_SNo 1 1) t0) (minus_SNo (add_SNo a b))) (add_SNo b (minus_SNo a))).
Use reflexivity.
We prove the intermediate claim Hhinvdef: hinv = graph R (λs0 : set ⇒ div_SNo (add_SNo (mul_SNo (add_SNo b (minus_SNo a)) s0) (add_SNo a b)) (add_SNo 1 1)).
Use reflexivity.
We prove the intermediate claim Hht: apply_fun h t = div_SNo num den.
rewrite the current goal using Hhdef (from left to right).
rewrite the current goal using (apply_fun_graph R (λt0 : set ⇒ div_SNo (add_SNo (mul_SNo (add_SNo 1 1) t0) (minus_SNo (add_SNo a b))) (add_SNo b (minus_SNo a))) t HtR) (from left to right).
Use reflexivity.
We prove the intermediate claim HhtR: apply_fun h t ∈ R.
rewrite the current goal using Hht (from left to right).
An exact proof term for the current goal is (real_div_SNo num HnumR den HdenR).
rewrite the current goal using Hhinvdef (from left to right).
rewrite the current goal using (apply_fun_graph R (λs0 : set ⇒ div_SNo (add_SNo (mul_SNo (add_SNo b (minus_SNo a)) s0) (add_SNo a b)) (add_SNo 1 1)) (apply_fun h t) HhtR) (from left to right).
rewrite the current goal using Hht (from left to right).
We prove the intermediate claim Hmul_cancel: mul_SNo den (div_SNo num den) = num.
An exact proof term for the current goal is (mul_div_SNo_invR num den HnumS HdenS Hden_ne0).
rewrite the current goal using Hmul_cancel (from left to right).
We prove the intermediate claim Hnumdef: num = add_SNo (mul_SNo two t) (minus_SNo ab).
Use reflexivity.
rewrite the current goal using Hnumdef (from left to right).
rewrite the current goal using (add_SNo_minus_R2' (mul_SNo two t) ab (SNo_mul_SNo two t HtwoS HtS) HabS) (from left to right).
We prove the intermediate claim Hdiv_eq: div_SNo (mul_SNo two t) two = t.
We prove the intermediate claim HmulId: mul_SNo two t = mul_SNo two t.
Use reflexivity.
An exact proof term for the current goal is (mul_div_SNo_nonzero_eq (mul_SNo two t) two t (SNo_mul_SNo two t HtwoS HtS) HtwoS HtS Htwo_ne0 HmulId).
An exact proof term for the current goal is Hdiv_eq.
Let s be given.
Assume Hs: s ∈ closed_interval (minus_SNo 1) 1.
We will prove apply_fun h (apply_fun hinv s) = s.
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (RleE_left a b Hab).
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is (RleE_right a b Hab).
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 HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim HsR: s ∈ R.
An exact proof term for the current goal is (closed_interval_sub_R (minus_SNo 1) 1 s Hs).
We prove the intermediate claim HsS: SNo s.
An exact proof term for the current goal is (real_SNo s HsR).
Set den to be the term add_SNo b (minus_SNo a).
Set two to be the term add_SNo 1 1.
Set ab to be the term add_SNo a b.
We prove the intermediate claim HabR: ab ∈ R.
An exact proof term for the current goal is (real_add_SNo a HaR b HbR).
We prove the intermediate claim HabS: SNo ab.
An exact proof term for the current goal is (real_SNo ab HabR).
We prove the intermediate claim HdenR: den ∈ R.
An exact proof term for the current goal is (real_add_SNo b HbR (minus_SNo a) (real_minus_SNo a HaR)).
We prove the intermediate claim HdenS: SNo den.
An exact proof term for the current goal is (real_SNo den HdenR).
We prove the intermediate claim HtwoS: SNo two.
An exact proof term for the current goal is (SNo_add_SNo 1 1 SNo_1 SNo_1).
We prove the intermediate claim Htwo_ne0: two ≠ 0.
Assume Htwo0: two = 0.
We prove the intermediate claim Htwo2: two = 2.
rewrite the current goal using (add_SNo_1_1_2) (from left to right).
Use reflexivity.
We prove the intermediate claim H20: 2 = 0.
rewrite the current goal using Htwo2 (from right to left) at position 1.
An exact proof term for the current goal is Htwo0.
An exact proof term for the current goal is (neq_2_0 H20).
We prove the intermediate claim Hden_ne0: den ≠ 0.
Assume Hden0: den = 0.
We prove the intermediate claim Hmab: minus_SNo a ∈ R.
An exact proof term for the current goal is (real_minus_SNo a HaR).
We prove the intermediate claim HmabS: SNo (minus_SNo a).
An exact proof term for the current goal is (real_SNo (minus_SNo a) Hmab).
We prove the intermediate claim Hlhs0: add_SNo b (minus_SNo a) = add_SNo a (minus_SNo a).
rewrite the current goal using Hden0 (from left to right) at position 1.
rewrite the current goal using (add_SNo_minus_SNo_rinv a HaS) (from left to right).
Use reflexivity.
We prove the intermediate claim Hba: b = a.
An exact proof term for the current goal is (add_SNo_cancel_R b (minus_SNo a) a HbS HmabS HaS Hlhs0).
We prove the intermediate claim Habeq: a = b.
rewrite the current goal using Hba (from right to left).
Use reflexivity.
An exact proof term for the current goal is (Hneq Habeq).
We prove the intermediate claim Hhdef: h = graph R (λt0 : set ⇒ div_SNo (add_SNo (mul_SNo (add_SNo 1 1) t0) (minus_SNo (add_SNo a b))) (add_SNo b (minus_SNo a))).
Use reflexivity.
We prove the intermediate claim Hhinvdef: hinv = graph R (λs0 : set ⇒ div_SNo (add_SNo (mul_SNo (add_SNo b (minus_SNo a)) s0) (add_SNo a b)) (add_SNo 1 1)).
Use reflexivity.
We prove the intermediate claim Hhinvs: apply_fun hinv s = div_SNo (add_SNo (mul_SNo den s) ab) two.
rewrite the current goal using Hhinvdef (from left to right).
rewrite the current goal using (apply_fun_graph R (λs0 : set ⇒ div_SNo (add_SNo (mul_SNo (add_SNo b (minus_SNo a)) s0) (add_SNo a b)) (add_SNo 1 1)) s HsR) (from left to right).
Use reflexivity.
We prove the intermediate claim HhinvsR: apply_fun hinv s ∈ R.
rewrite the current goal using Hhinvs (from left to right).
We prove the intermediate claim HmulR: mul_SNo den s ∈ R.
An exact proof term for the current goal is (real_mul_SNo den HdenR s HsR).
We prove the intermediate claim HnumR: add_SNo (mul_SNo den s) ab ∈ R.
An exact proof term for the current goal is (real_add_SNo (mul_SNo den s) HmulR ab HabR).
An exact proof term for the current goal is (real_div_SNo (add_SNo (mul_SNo den s) ab) HnumR two (real_add_SNo 1 real_1 1 real_1)).
rewrite the current goal using Hhdef (from left to right).
rewrite the current goal using (apply_fun_graph R (λt0 : set ⇒ div_SNo (add_SNo (mul_SNo (add_SNo 1 1) t0) (minus_SNo (add_SNo a b))) (add_SNo b (minus_SNo a))) (apply_fun hinv s) HhinvsR) (from left to right).
rewrite the current goal using Hhinvs (from left to right).
We prove the intermediate claim Hmul2_cancel: mul_SNo two (div_SNo (add_SNo (mul_SNo den s) ab) two) = add_SNo (mul_SNo den s) ab.
An exact proof term for the current goal is (mul_div_SNo_invR (add_SNo (mul_SNo den s) ab) two (SNo_add_SNo (mul_SNo den s) ab (SNo_mul_SNo den s HdenS HsS) HabS) HtwoS Htwo_ne0).
rewrite the current goal using Hmul2_cancel (from left to right).
rewrite the current goal using (add_SNo_minus_R2 (mul_SNo den s) ab (SNo_mul_SNo den s HdenS HsS) HabS) (from left to right).
We prove the intermediate claim Hdiv_eq: div_SNo (mul_SNo den s) den = s.
We prove the intermediate claim HmulId: mul_SNo den s = mul_SNo den s.
Use reflexivity.
An exact proof term for the current goal is (mul_div_SNo_nonzero_eq (mul_SNo den s) den s (SNo_mul_SNo den s HdenS HsS) HdenS HsS Hden_ne0 HmulId).
rewrite the current goal using Hdiv_eq (from left to right).
Use reflexivity.
∎