Let a, b and c be given.
Assume HaR: a ∈ R.
Assume HbR: b ∈ R.
Assume HcR: c ∈ R.
Assume Hbne: b ≠ 0.
Set gdiv to be the term graph R (λx : set ⇒ div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b).
Set Tx to be the term R_lower_limit_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_lower_limit_topology_is_topology.
We prove the intermediate claim HincStd: R_standard_topology ⊆ Tx.
An exact proof term for the current goal is R_lower_limit_finer_than_R_standard.
We prove the intermediate claim HS: subbasis_on R S.
An exact proof term for the current goal is (open_rays_subbasis_is_subbasis R).
We prove the intermediate claim Hgen: generated_topology_from_subbasis R S = R_standard_topology.
rewrite the current goal using open_rays_subbasis_for_order_topology_R (from left to right).
rewrite the current goal using standard_topology_is_order_topology (from left to right).
Use reflexivity.
We prove the intermediate claim Hfun: function_on gdiv R R.
Let x be given.
Assume HxR: x ∈ R.
We will prove apply_fun gdiv x ∈ R.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
We prove the intermediate claim HaReal: a ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HaR.
We prove the intermediate claim HbReal: b ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HbR.
We prove the intermediate claim HcReal: c ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HcR.
We prove the intermediate claim HxReal: x ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HxR.
We prove the intermediate claim HaxReal: mul_SNo a x ∈ real.
An exact proof term for the current goal is (real_mul_SNo a HaReal x HxReal).
We prove the intermediate claim HmxReal: minus_SNo (mul_SNo a x) ∈ real.
An exact proof term for the current goal is (real_minus_SNo (mul_SNo a x) HaxReal).
We prove the intermediate claim HnumReal: add_SNo c (minus_SNo (mul_SNo a x)) ∈ real.
An exact proof term for the current goal is (real_add_SNo c HcReal (minus_SNo (mul_SNo a x)) HmxReal).
We prove the intermediate claim HdivReal: div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b ∈ real.
An exact proof term for the current goal is (real_div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) HnumReal b HbReal).
rewrite the current goal using HdefR (from left to right).
rewrite the current goal using (apply_fun_graph R (λx0 : set ⇒ div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) b) x HxR) (from left to right).
An exact proof term for the current goal is HdivReal.
We prove the intermediate claim Hpre_upper: ∀d : set, d ∈ R → preimage_of R gdiv (open_ray_upper R d) ∈ Tx.
Let d be given.
Assume HdR: d ∈ R.
Apply (xm (a = 0)) to the current goal.
Assume Ha0: a = 0.
Set y0 to be the term div_SNo c b.
We prove the intermediate claim Hy0R: y0 ∈ R.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
We prove the intermediate claim HbReal: b ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HbR.
We prove the intermediate claim HcReal: c ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HcR.
We prove the intermediate claim Hy0Real: y0 ∈ real.
An exact proof term for the current goal is (real_div_SNo c HcReal b HbReal).
rewrite the current goal using HdefR (from left to right).
An exact proof term for the current goal is Hy0Real.
We prove the intermediate claim Hgapply: ∀x : set, x ∈ R → apply_fun gdiv x = y0.
Let x be given.
Assume HxR: x ∈ R.
rewrite the current goal using (apply_fun_graph R (λx0 : set ⇒ div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) b) x HxR) (from left to right).
rewrite the current goal using Ha0 (from left to right).
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
We prove the intermediate claim HxReal: x ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HxR.
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxReal).
We prove the intermediate claim HcReal: c ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HcR.
We prove the intermediate claim HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcReal).
rewrite the current goal using (mul_SNo_zeroL x HxS) (from left to right).
rewrite the current goal using (minus_SNo_0) (from left to right) at position 1.
rewrite the current goal using (add_SNo_0R c HcS) (from left to right) at position 1.
Use reflexivity.
Apply (xm (Rlt d y0)) to the current goal.
Assume Hdlt: Rlt d y0.
We prove the intermediate claim HeqPre: preimage_of R gdiv (open_ray_upper R d) = R.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ preimage_of R gdiv (open_ray_upper R d).
An exact proof term for the current goal is (SepE1 R (λu : set ⇒ apply_fun gdiv u ∈ open_ray_upper R d) x Hx).
Let x be given.
Assume HxR: x ∈ R.
We will prove x ∈ preimage_of R gdiv (open_ray_upper R d).
We prove the intermediate claim HyIn: apply_fun gdiv x ∈ open_ray_upper R d.
rewrite the current goal using (Hgapply x HxR) (from left to right).
We prove the intermediate claim Hraydef: open_ray_upper R d = {t ∈ R|order_rel R d t}.
Use reflexivity.
rewrite the current goal using Hraydef (from left to right).
Apply SepI to the current goal.
An exact proof term for the current goal is Hy0R.
An exact proof term for the current goal is (Rlt_implies_order_rel_R d y0 Hdlt).
An exact proof term for the current goal is (SepI R (λu : set ⇒ apply_fun gdiv u ∈ open_ray_upper R d) x HxR HyIn).
rewrite the current goal using HeqPre (from left to right).
An exact proof term for the current goal is (topology_has_X R Tx HTx).
Assume Hnlt: ¬ (Rlt d y0).
We prove the intermediate claim HeqPre: preimage_of R gdiv (open_ray_upper R d) = Empty.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ preimage_of R gdiv (open_ray_upper R d).
Apply FalseE to the current goal.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λu : set ⇒ apply_fun gdiv u ∈ open_ray_upper R d) x Hx).
We prove the intermediate claim Himg: apply_fun gdiv x ∈ open_ray_upper R d.
An exact proof term for the current goal is (SepE2 R (λu : set ⇒ apply_fun gdiv u ∈ open_ray_upper R d) x Hx).
We prove the intermediate claim Hrel: order_rel R d (apply_fun gdiv x).
An exact proof term for the current goal is (SepE2 R (λy : set ⇒ order_rel R d y) (apply_fun gdiv x) Himg).
We prove the intermediate claim Hdlt: Rlt d (apply_fun gdiv x).
An exact proof term for the current goal is (order_rel_R_implies_Rlt d (apply_fun gdiv x) Hrel).
We prove the intermediate claim HyEq: apply_fun gdiv x = y0.
An exact proof term for the current goal is (Hgapply x HxR).
We prove the intermediate claim Hdlt2: Rlt d y0.
rewrite the current goal using HyEq (from right to left).
An exact proof term for the current goal is Hdlt.
An exact proof term for the current goal is (Hnlt Hdlt2).
Let x be given.
Assume HxE: x ∈ Empty.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE x HxE).
rewrite the current goal using HeqPre (from left to right).
An exact proof term for the current goal is (topology_has_empty R Tx HTx).
Assume Ha0: ¬ (a = 0).
Set rhs to be the term add_SNo c (minus_SNo (mul_SNo b d)).
Set x0 to be the term div_SNo rhs a.
We prove the intermediate claim Ha0': a ≠ 0.
Assume Heq: a = 0.
An exact proof term for the current goal is (Ha0 Heq).
We prove the intermediate claim Hx0R: x0 ∈ R.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
We prove the intermediate claim HaReal: a ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HaR.
We prove the intermediate claim HbReal: b ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HbR.
We prove the intermediate claim HdReal: d ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HdR.
We prove the intermediate claim HcReal: c ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HcR.
We prove the intermediate claim HbdReal: mul_SNo b d ∈ real.
An exact proof term for the current goal is (real_mul_SNo b HbReal d HdReal).
We prove the intermediate claim HmbdReal: minus_SNo (mul_SNo b d) ∈ real.
An exact proof term for the current goal is (real_minus_SNo (mul_SNo b d) HbdReal).
We prove the intermediate claim HrhsReal: rhs ∈ real.
An exact proof term for the current goal is (real_add_SNo c HcReal (minus_SNo (mul_SNo b d)) HmbdReal).
We prove the intermediate claim Hx0Real: x0 ∈ real.
An exact proof term for the current goal is (real_div_SNo rhs HrhsReal a HaReal).
rewrite the current goal using HdefR (from left to right).
An exact proof term for the current goal is Hx0Real.
We prove the intermediate claim Hyx0eq: div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) b = d.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
We prove the intermediate claim HaReal: a ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HaR.
We prove the intermediate claim HbReal: b ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HbR.
We prove the intermediate claim HcReal: c ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HcR.
We prove the intermediate claim HdReal: d ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HdR.
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaReal).
We prove the intermediate claim HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbReal).
We prove the intermediate claim HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcReal).
We prove the intermediate claim HdS: SNo d.
An exact proof term for the current goal is (real_SNo d HdReal).
We prove the intermediate claim HrhsS: SNo rhs.
An exact proof term for the current goal is (SNo_add_SNo c (minus_SNo (mul_SNo b d)) HcS (SNo_minus_SNo (mul_SNo b d) (SNo_mul_SNo b d HbS HdS))).
We prove the intermediate claim Hmulax0: mul_SNo a x0 = rhs.
rewrite the current goal using (mul_div_SNo_invR rhs a HrhsS HaS Ha0') (from left to right).
Use reflexivity.
We prove the intermediate claim HnumEq: add_SNo c (minus_SNo (mul_SNo a x0)) = mul_SNo b d.
rewrite the current goal using Hmulax0 (from left to right).
We prove the intermediate claim Hneg: minus_SNo rhs = add_SNo (minus_SNo c) (minus_SNo (minus_SNo (mul_SNo b d))).
An exact proof term for the current goal is (minus_add_SNo_distr c (minus_SNo (mul_SNo b d)) HcS (SNo_minus_SNo (mul_SNo b d) (SNo_mul_SNo b d HbS HdS))).
We prove the intermediate claim Hinv: minus_SNo (minus_SNo (mul_SNo b d)) = mul_SNo b d.
An exact proof term for the current goal is (minus_SNo_invol (mul_SNo b d) (SNo_mul_SNo b d HbS HdS)).
rewrite the current goal using Hneg (from left to right).
rewrite the current goal using Hinv (from left to right) at position 1.
rewrite the current goal using (add_SNo_assoc c (minus_SNo c) (mul_SNo b d) HcS (SNo_minus_SNo c HcS) (SNo_mul_SNo b d HbS HdS)) (from left to right).
rewrite the current goal using (add_SNo_minus_SNo_rinv c HcS) (from left to right) at position 1.
rewrite the current goal using (add_SNo_0L (mul_SNo b d) (SNo_mul_SNo b d HbS HdS)) (from left to right).
Use reflexivity.
rewrite the current goal using HnumEq (from left to right).
Apply (mul_div_SNo_nonzero_eq (mul_SNo b d) b d (SNo_mul_SNo b d HbS HdS) HbS HdS Hbne) to the current goal.
Use reflexivity.
We prove the intermediate claim Hgdiv_x0: apply_fun gdiv x0 = d.
rewrite the current goal using (apply_fun_graph R (λx0 : set ⇒ div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) b) x0 Hx0R) (from left to right).
rewrite the current goal using Hyx0eq (from left to right).
Use reflexivity.
Set Pre to be the term preimage_of R gdiv (open_ray_upper R d).
Apply (xm (same_sign_nonzero_R a b)) to the current goal.
Assume Hsign: same_sign_nonzero_R a b.
We prove the intermediate claim HeqPre: Pre = open_ray_lower R x0.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ Pre.
We will prove x ∈ open_ray_lower R x0.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λu : set ⇒ apply_fun gdiv u ∈ open_ray_upper R d) x Hx).
We prove the intermediate claim Himg: apply_fun gdiv x ∈ open_ray_upper R d.
An exact proof term for the current goal is (SepE2 R (λu : set ⇒ apply_fun gdiv u ∈ open_ray_upper R d) x Hx).
We prove the intermediate claim Hrel: order_rel R d (apply_fun gdiv x).
An exact proof term for the current goal is (SepE2 R (λy : set ⇒ order_rel R d y) (apply_fun gdiv x) Himg).
We prove the intermediate claim Hdlt_app: Rlt d (apply_fun gdiv x).
An exact proof term for the current goal is (order_rel_R_implies_Rlt d (apply_fun gdiv x) Hrel).
We prove the intermediate claim Hdlt_y: Rlt d (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b).
rewrite the current goal using (apply_fun_graph R (λx0 : set ⇒ div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) b) x HxR) (from right to left).
An exact proof term for the current goal is Hdlt_app.
We prove the intermediate claim HxReal: x ∈ real.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HxR.
We prove the intermediate claim Hx0Real: x0 ∈ real.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is Hx0R.
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxReal).
We prove the intermediate claim Hx0S: SNo x0.
An exact proof term for the current goal is (real_SNo x0 Hx0Real).
Apply (SNoLt_trichotomy_or_impred x x0 HxS Hx0S (x ∈ open_ray_lower R x0)) to the current goal.
Assume Hxlt: x < x0.
We prove the intermediate claim Hlt: Rlt x x0.
An exact proof term for the current goal is (RltI x x0 HxR Hx0R Hxlt).
We prove the intermediate claim Hraydef: open_ray_lower R x0 = {t ∈ R|order_rel R t x0}.
Use reflexivity.
rewrite the current goal using Hraydef (from left to right).
Apply SepI to the current goal.
An exact proof term for the current goal is HxR.
An exact proof term for the current goal is (Rlt_implies_order_rel_R x x0 Hlt).
Assume Hxeq: x = x0.
Apply FalseE to the current goal.
We prove the intermediate claim Hdlt0: Rlt d (apply_fun gdiv x0).
rewrite the current goal using Hxeq (from right to left).
An exact proof term for the current goal is Hdlt_app.
We prove the intermediate claim Hdltdd: Rlt d d.
rewrite the current goal using Hgdiv_x0 (from right to left) at position 2.
An exact proof term for the current goal is Hdlt0.
An exact proof term for the current goal is (not_Rlt_refl d HdR Hdltdd).
Assume Hx0lt: x0 < x.
Apply FalseE to the current goal.
We prove the intermediate claim Hx0ltR: Rlt x0 x.
An exact proof term for the current goal is (RltI x0 x Hx0R HxR Hx0lt).
We prove the intermediate claim Hdec: Rlt (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) (div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) b).
An exact proof term for the current goal is (affine_line_R2_param_by_x_y_decreases_same_sign a b c x0 x HaR HbR HcR Hbne Hsign Hx0R HxR Hx0ltR).
We prove the intermediate claim Hdlt0: Rlt (div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) b) (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b).
rewrite the current goal using Hyx0eq (from left to right) at position 1.
An exact proof term for the current goal is Hdlt_y.
An exact proof term for the current goal is (not_Rlt_sym (div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) b) (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) Hdlt0 Hdec).
Let x be given.
Assume Hx: x ∈ open_ray_lower R x0.
We will prove x ∈ Pre.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λu : set ⇒ order_rel R u x0) x Hx).
We prove the intermediate claim Hrel: order_rel R x x0.
An exact proof term for the current goal is (SepE2 R (λu : set ⇒ order_rel R u x0) x Hx).
We prove the intermediate claim Hlt: Rlt x x0.
An exact proof term for the current goal is (order_rel_R_implies_Rlt x x0 Hrel).
We prove the intermediate claim Hdec: Rlt (div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) b) (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b).
An exact proof term for the current goal is (affine_line_R2_param_by_x_y_decreases_same_sign a b c x x0 HaR HbR HcR Hbne Hsign HxR Hx0R Hlt).
We prove the intermediate claim Hdlt_y: Rlt d (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b).
rewrite the current goal using Hyx0eq (from right to left) at position 1.
An exact proof term for the current goal is Hdec.
We prove the intermediate claim Himg: apply_fun gdiv x ∈ open_ray_upper R d.
rewrite the current goal using (apply_fun_graph R (λx0 : set ⇒ div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) b) x HxR) (from left to right).
We prove the intermediate claim Hraydef: open_ray_upper R d = {t ∈ R|order_rel R d t}.
Use reflexivity.
rewrite the current goal using Hraydef (from left to right).
Apply SepI to the current goal.
We prove the intermediate claim HdivR: div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b ∈ R.
rewrite the current goal using (apply_fun_graph R (λx0 : set ⇒ div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) b) x HxR) (from right to left).
An exact proof term for the current goal is (Hfun x HxR).
An exact proof term for the current goal is HdivR.
An exact proof term for the current goal is (Rlt_implies_order_rel_R d (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) Hdlt_y).
An exact proof term for the current goal is (SepI R (λu : set ⇒ apply_fun gdiv u ∈ open_ray_upper R d) x HxR Himg).
rewrite the current goal using HeqPre (from left to right).
We prove the intermediate claim HrayStd: open_ray_lower R x0 ∈ R_standard_topology.
We prove the intermediate claim HrInS: open_ray_lower R x0 ∈ S.
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.
rewrite the current goal using HSdef (from left to right).
Apply binunionI1 to the current goal.
Apply binunionI2 to the current goal.
Apply (SepI (𝒫 R) (λI0 : set ⇒ ∃b0 ∈ R, I0 = open_ray_lower R b0) (open_ray_lower R x0)) to the current goal.
Apply PowerI to the current goal.
Let t be given.
Assume Ht: t ∈ open_ray_lower R x0.
An exact proof term for the current goal is (SepE1 R (λu : set ⇒ order_rel R u x0) t Ht).
We use x0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hx0R.
Use reflexivity.
We prove the intermediate claim HrGen: open_ray_lower R x0 ∈ generated_topology_from_subbasis R S.
An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis R S (open_ray_lower R x0) HS HrInS).
rewrite the current goal using Hgen (from right to left).
An exact proof term for the current goal is HrGen.
An exact proof term for the current goal is (HincStd (open_ray_lower R x0) HrayStd).
Assume Hnotsign: ¬ (same_sign_nonzero_R a b).
Set mb to be the term minus_SNo b.
We prove the intermediate claim HmbR: mb ∈ R.
An exact proof term for the current goal is (real_minus_SNo b HbR).
We prove the intermediate claim Hmb0: mb ≠ 0.
Assume Hmb0eq: mb = 0.
We prove the intermediate claim Hb0eq: b = 0.
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 Hmbdef: mb = minus_SNo b.
Use reflexivity.
rewrite the current goal using (minus_SNo_invol b HbS) (from right to left) at position 1.
rewrite the current goal using Hmbdef (from right to left) at position 1.
rewrite the current goal using Hmb0eq (from left to right).
rewrite the current goal using minus_SNo_0 (from left to right).
Use reflexivity.
An exact proof term for the current goal is (Hbne Hb0eq).
We prove the intermediate claim Hsignmb: same_sign_nonzero_R a mb.
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).
Apply (SNoLt_trichotomy_or_impred a 0 HaS SNo_0 (same_sign_nonzero_R a mb)) to the current goal.
Assume Halt0: a < 0.
Apply (SNoLt_trichotomy_or_impred b 0 HbS SNo_0 (same_sign_nonzero_R a mb)) to the current goal.
Assume Hblt0: b < 0.
Apply FalseE to the current goal.
We prove the intermediate claim Halt0R: Rlt a 0.
An exact proof term for the current goal is (RltI a 0 HaR real_0 Halt0).
We prove the intermediate claim Hblt0R: Rlt b 0.
An exact proof term for the current goal is (RltI b 0 HbR real_0 Hblt0).
We prove the intermediate claim Hss: same_sign_nonzero_R a b.
An exact proof term for the current goal is (orIR (Rlt 0 a ∧ Rlt 0 b) (Rlt a 0 ∧ Rlt b 0) (andI (Rlt a 0) (Rlt b 0) Halt0R Hblt0R)).
An exact proof term for the current goal is (Hnotsign Hss).
Assume Hb0eq: b = 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hbne Hb0eq).
Assume H0blt: 0 < b.
We prove the intermediate claim Halt0R: Rlt a 0.
An exact proof term for the current goal is (RltI a 0 HaR real_0 Halt0).
We prove the intermediate claim HmbS: SNo mb.
An exact proof term for the current goal is (SNo_minus_SNo b HbS).
We prove the intermediate claim Hmblt0: mb < 0.
We prove the intermediate claim Hflip: minus_SNo b < minus_SNo 0.
An exact proof term for the current goal is (minus_SNo_Lt_contra 0 b SNo_0 HbS H0blt).
rewrite the current goal using (minus_SNo_0) (from right to left) at position 1.
An exact proof term for the current goal is Hflip.
We prove the intermediate claim HmbLt0R: Rlt mb 0.
An exact proof term for the current goal is (RltI mb 0 HmbR real_0 Hmblt0).
An exact proof term for the current goal is (orIR (Rlt 0 a ∧ Rlt 0 mb) (Rlt a 0 ∧ Rlt mb 0) (andI (Rlt a 0) (Rlt mb 0) Halt0R HmbLt0R)).
Assume Ha0eq: a = 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Ha0 Ha0eq).
Assume H0alt: 0 < a.
Apply (SNoLt_trichotomy_or_impred b 0 HbS SNo_0 (same_sign_nonzero_R a mb)) to the current goal.
Assume Hblt0: b < 0.
We prove the intermediate claim H0aR: Rlt 0 a.
An exact proof term for the current goal is (RltI 0 a real_0 HaR H0alt).
We prove the intermediate claim HmbS: SNo mb.
An exact proof term for the current goal is (SNo_minus_SNo b HbS).
We prove the intermediate claim H0mblt: 0 < mb.
We prove the intermediate claim Hflip: minus_SNo 0 < minus_SNo b.
An exact proof term for the current goal is (minus_SNo_Lt_contra b 0 HbS SNo_0 Hblt0).
rewrite the current goal using (minus_SNo_0) (from right to left) at position 1.
An exact proof term for the current goal is Hflip.
We prove the intermediate claim H0mbR: Rlt 0 mb.
An exact proof term for the current goal is (RltI 0 mb real_0 HmbR H0mblt).
An exact proof term for the current goal is (orIL (Rlt 0 a ∧ Rlt 0 mb) (Rlt a 0 ∧ Rlt mb 0) (andI (Rlt 0 a) (Rlt 0 mb) H0aR H0mbR)).
Assume Hb0eq: b = 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hbne Hb0eq).
Assume H0blt: 0 < b.
Apply FalseE to the current goal.
We prove the intermediate claim H0aR: Rlt 0 a.
An exact proof term for the current goal is (RltI 0 a real_0 HaR H0alt).
We prove the intermediate claim H0bR: Rlt 0 b.
An exact proof term for the current goal is (RltI 0 b real_0 HbR H0blt).
We prove the intermediate claim Hss: same_sign_nonzero_R a b.
An exact proof term for the current goal is (orIL (Rlt 0 a ∧ Rlt 0 b) (Rlt a 0 ∧ Rlt b 0) (andI (Rlt 0 a) (Rlt 0 b) H0aR H0bR)).
An exact proof term for the current goal is (Hnotsign Hss).
We prove the intermediate claim HdivMinusDen: ∀t : set, t ∈ R → div_SNo t mb = minus_SNo (div_SNo t b).
Let t be given.
Assume HtR: t ∈ R.
We prove the intermediate claim HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim Hmbdef: mb = minus_SNo b.
Use reflexivity.
rewrite the current goal using Hmbdef (from left to right).
We prove the intermediate claim Hrecip: recip_SNo (minus_SNo b) = minus_SNo (recip_SNo b).
Apply (SNoLt_trichotomy_or_impred b 0 HbS SNo_0 (recip_SNo (minus_SNo b) = minus_SNo (recip_SNo b))) to the current goal.
Assume Hblt0: b < 0.
We prove the intermediate claim HmbS: SNo (minus_SNo b).
An exact proof term for the current goal is (SNo_minus_SNo b HbS).
We prove the intermediate claim H0mb: 0 < minus_SNo b.
We prove the intermediate claim Htmp: minus_SNo 0 < minus_SNo b.
An exact proof term for the current goal is (minus_SNo_Lt_contra b 0 HbS SNo_0 Hblt0).
rewrite the current goal using (minus_SNo_0) (from right to left) at position 1.
An exact proof term for the current goal is Htmp.
rewrite the current goal using (recip_SNo_poscase (minus_SNo b) H0mb) (from left to right).
rewrite the current goal using (recip_SNo_negcase b HbS Hblt0) (from left to right).
We prove the intermediate claim HtPosS: SNo (recip_SNo_pos (minus_SNo b)).
An exact proof term for the current goal is (SNo_recip_SNo_pos (minus_SNo b) HmbS H0mb).
rewrite the current goal using (minus_SNo_invol (recip_SNo_pos (minus_SNo b)) HtPosS) (from left to right).
Use reflexivity.
Assume Hb0eq: b = 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hbne Hb0eq).
Assume H0blt: 0 < b.
We prove the intermediate claim HmbS: SNo (minus_SNo b).
An exact proof term for the current goal is (SNo_minus_SNo b HbS).
We prove the intermediate claim Hmblt0: minus_SNo b < 0.
We prove the intermediate claim Htmp: minus_SNo b < minus_SNo 0.
An exact proof term for the current goal is (minus_SNo_Lt_contra 0 b SNo_0 HbS H0blt).
rewrite the current goal using (minus_SNo_0) (from right to left) at position 1.
An exact proof term for the current goal is Htmp.
rewrite the current goal using (recip_SNo_negcase (minus_SNo b) HmbS Hmblt0) (from left to right).
rewrite the current goal using (minus_SNo_invol b HbS) (from left to right) at position 1.
rewrite the current goal using (recip_SNo_poscase b H0blt) (from left to right).
Use reflexivity.
We prove the intermediate claim Hdivdef1: div_SNo t (minus_SNo b) = mul_SNo t (recip_SNo (minus_SNo b)).
Use reflexivity.
We prove the intermediate claim Hdivdef2: div_SNo t b = mul_SNo t (recip_SNo b).
Use reflexivity.
rewrite the current goal using Hdivdef1 (from left to right).
rewrite the current goal using Hdivdef2 (from left to right).
rewrite the current goal using Hrecip (from left to right).
An exact proof term for the current goal is (mul_SNo_minus_distrR t (recip_SNo b) HtS (SNo_recip_SNo b HbS)).
We prove the intermediate claim HeqPre: Pre = open_ray_upper R x0.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ Pre.
We will prove x ∈ open_ray_upper R x0.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λu : set ⇒ apply_fun gdiv u ∈ open_ray_upper R d) x Hx).
We prove the intermediate claim Himg: apply_fun gdiv x ∈ open_ray_upper R d.
An exact proof term for the current goal is (SepE2 R (λu : set ⇒ apply_fun gdiv u ∈ open_ray_upper R d) x Hx).
We prove the intermediate claim Hrel: order_rel R d (apply_fun gdiv x).
An exact proof term for the current goal is (SepE2 R (λy : set ⇒ order_rel R d y) (apply_fun gdiv x) Himg).
We prove the intermediate claim Hdlt_app: Rlt d (apply_fun gdiv x).
An exact proof term for the current goal is (order_rel_R_implies_Rlt d (apply_fun gdiv x) Hrel).
We prove the intermediate claim Hdlt_y: Rlt d (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b).
rewrite the current goal using (apply_fun_graph R (λx0 : set ⇒ div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) b) x HxR) (from right to left).
An exact proof term for the current goal is Hdlt_app.
We prove the intermediate claim HxReal: x ∈ real.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HxR.
We prove the intermediate claim Hx0Real: x0 ∈ real.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is Hx0R.
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxReal).
We prove the intermediate claim Hx0S: SNo x0.
An exact proof term for the current goal is (real_SNo x0 Hx0Real).
Apply (SNoLt_trichotomy_or_impred x x0 HxS Hx0S (x ∈ open_ray_upper R x0)) to the current goal.
Assume Hxlt: x < x0.
Apply FalseE to the current goal.
We prove the intermediate claim HxltR: Rlt x x0.
An exact proof term for the current goal is (RltI x x0 HxR Hx0R Hxlt).
We prove the intermediate claim HdecNeg: Rlt (div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) mb) (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) mb).
An exact proof term for the current goal is (affine_line_R2_param_by_x_y_decreases_same_sign a mb c x x0 HaR HmbR HcR Hmb0 Hsignmb HxR Hx0R HxltR).
We prove the intermediate claim HnumxR: add_SNo c (minus_SNo (mul_SNo a x)) ∈ R.
We prove the intermediate claim HaxR: mul_SNo a x ∈ R.
An exact proof term for the current goal is (real_mul_SNo a HaR x HxR).
We prove the intermediate claim HmxR: minus_SNo (mul_SNo a x) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (mul_SNo a x) HaxR).
An exact proof term for the current goal is (real_add_SNo c HcR (minus_SNo (mul_SNo a x)) HmxR).
We prove the intermediate claim Hnumx0R: add_SNo c (minus_SNo (mul_SNo a x0)) ∈ R.
We prove the intermediate claim Hax0R2: mul_SNo a x0 ∈ R.
An exact proof term for the current goal is (real_mul_SNo a HaR x0 Hx0R).
We prove the intermediate claim Hmx0R: minus_SNo (mul_SNo a x0) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (mul_SNo a x0) Hax0R2).
An exact proof term for the current goal is (real_add_SNo c HcR (minus_SNo (mul_SNo a x0)) Hmx0R).
We prove the intermediate claim Hynegx: div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) mb = minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b).
An exact proof term for the current goal is (HdivMinusDen (add_SNo c (minus_SNo (mul_SNo a x))) HnumxR).
We prove the intermediate claim Hynegx0: div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) mb = minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) b).
An exact proof term for the current goal is (HdivMinusDen (add_SNo c (minus_SNo (mul_SNo a x0))) Hnumx0R).
We prove the intermediate claim Hltneg: Rlt (minus_SNo d) (minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b)).
rewrite the current goal using Hyx0eq (from right to left) at position 1.
rewrite the current goal using Hynegx0 (from right to left) at position 1.
rewrite the current goal using Hynegx (from right to left) at position 1.
An exact proof term for the current goal is HdecNeg.
We prove the intermediate claim HltnegS: minus_SNo d < minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b).
An exact proof term for the current goal is (RltE_lt (minus_SNo d) (minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b)) Hltneg).
We prove the intermediate claim HdS: SNo d.
An exact proof term for the current goal is (real_SNo d HdR).
We prove the intermediate claim HyR: div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b ∈ R.
An exact proof term for the current goal is (RltE_right d (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) Hdlt_y).
We prove the intermediate claim HyS: SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b).
An exact proof term for the current goal is (real_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) HyR).
We prove the intermediate claim HmdS: SNo (minus_SNo d).
An exact proof term for the current goal is (SNo_minus_SNo d HdS).
We prove the intermediate claim HmyS: SNo (minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b)).
An exact proof term for the current goal is (SNo_minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) HyS).
We prove the intermediate claim HyltD: div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b < d.
We prove the intermediate claim Hflip: minus_SNo d < minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) → div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b < d.
Assume Htmp.
We prove the intermediate claim Htmp2: minus_SNo (minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b)) < minus_SNo (minus_SNo d).
An exact proof term for the current goal is (minus_SNo_Lt_contra (minus_SNo d) (minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b)) HmdS HmyS Htmp).
rewrite the current goal using (minus_SNo_invol (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) HyS) (from right to left) at position 1.
rewrite the current goal using (minus_SNo_invol d HdS) (from right to left) at position 1.
An exact proof term for the current goal is Htmp2.
An exact proof term for the current goal is (Hflip HltnegS).
We prove the intermediate claim HyltR: Rlt (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) d.
Apply (RltI (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) d HyR HdR HyltD) to the current goal.
An exact proof term for the current goal is (not_Rlt_sym d (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) Hdlt_y HyltR).
Assume Hxeq: x = x0.
Apply FalseE to the current goal.
We prove the intermediate claim Hdlt0: Rlt d (apply_fun gdiv x0).
rewrite the current goal using Hxeq (from right to left).
An exact proof term for the current goal is Hdlt_app.
We prove the intermediate claim Hdltdd: Rlt d d.
rewrite the current goal using Hgdiv_x0 (from right to left) at position 2.
An exact proof term for the current goal is Hdlt0.
An exact proof term for the current goal is (not_Rlt_refl d HdR Hdltdd).
Assume Hx0lt: x0 < x.
We prove the intermediate claim Hx0ltR: Rlt x0 x.
An exact proof term for the current goal is (RltI x0 x Hx0R HxR Hx0lt).
We prove the intermediate claim Hraydef: open_ray_upper R x0 = {t ∈ R|order_rel R x0 t}.
Use reflexivity.
rewrite the current goal using Hraydef (from left to right).
Apply SepI to the current goal.
An exact proof term for the current goal is HxR.
An exact proof term for the current goal is (Rlt_implies_order_rel_R x0 x Hx0ltR).
Let x be given.
Assume Hx: x ∈ open_ray_upper R x0.
We will prove x ∈ Pre.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λu : set ⇒ order_rel R x0 u) x Hx).
We prove the intermediate claim Hrel: order_rel R x0 x.
An exact proof term for the current goal is (SepE2 R (λu : set ⇒ order_rel R x0 u) x Hx).
We prove the intermediate claim Hx0ltR: Rlt x0 x.
An exact proof term for the current goal is (order_rel_R_implies_Rlt x0 x Hrel).
We prove the intermediate claim HdecNeg: Rlt (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) mb) (div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) mb).
An exact proof term for the current goal is (affine_line_R2_param_by_x_y_decreases_same_sign a mb c x0 x HaR HmbR HcR Hmb0 Hsignmb Hx0R HxR Hx0ltR).
We prove the intermediate claim HnumxR: add_SNo c (minus_SNo (mul_SNo a x)) ∈ R.
We prove the intermediate claim HaxR: mul_SNo a x ∈ R.
An exact proof term for the current goal is (real_mul_SNo a HaR x HxR).
We prove the intermediate claim HmxR: minus_SNo (mul_SNo a x) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (mul_SNo a x) HaxR).
An exact proof term for the current goal is (real_add_SNo c HcR (minus_SNo (mul_SNo a x)) HmxR).
We prove the intermediate claim Hnumx0R: add_SNo c (minus_SNo (mul_SNo a x0)) ∈ R.
We prove the intermediate claim Hax0R2: mul_SNo a x0 ∈ R.
An exact proof term for the current goal is (real_mul_SNo a HaR x0 Hx0R).
We prove the intermediate claim Hmx0R: minus_SNo (mul_SNo a x0) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (mul_SNo a x0) Hax0R2).
An exact proof term for the current goal is (real_add_SNo c HcR (minus_SNo (mul_SNo a x0)) Hmx0R).
We prove the intermediate claim Hynegx: div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) mb = minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b).
An exact proof term for the current goal is (HdivMinusDen (add_SNo c (minus_SNo (mul_SNo a x))) HnumxR).
We prove the intermediate claim Hynegx0: div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) mb = minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) b).
An exact proof term for the current goal is (HdivMinusDen (add_SNo c (minus_SNo (mul_SNo a x0))) Hnumx0R).
We prove the intermediate claim Hltneg: minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) < minus_SNo d.
We prove the intermediate claim HltR: Rlt (minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b)) (minus_SNo d).
rewrite the current goal using Hynegx (from right to left) at position 1.
rewrite the current goal using Hyx0eq (from right to left).
rewrite the current goal using Hynegx0 (from right to left).
An exact proof term for the current goal is HdecNeg.
An exact proof term for the current goal is (RltE_lt (minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b)) (minus_SNo d) HltR).
We prove the intermediate claim HdS: SNo d.
An exact proof term for the current goal is (real_SNo d HdR).
We prove the intermediate claim HyR: div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b ∈ R.
An exact proof term for the current goal is (real_div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) HnumxR b HbR).
We prove the intermediate claim HyS: SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b).
An exact proof term for the current goal is (real_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) HyR).
We prove the intermediate claim HmdS: SNo (minus_SNo d).
An exact proof term for the current goal is (SNo_minus_SNo d HdS).
We prove the intermediate claim HmyS: SNo (minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b)).
An exact proof term for the current goal is (SNo_minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) HyS).
We prove the intermediate claim HdltY: d < div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b.
We prove the intermediate claim Hflip: minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) < minus_SNo d → d < div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b.
Assume Htmp.
We prove the intermediate claim Htmp2: minus_SNo (minus_SNo d) < minus_SNo (minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b)).
An exact proof term for the current goal is (minus_SNo_Lt_contra (minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b)) (minus_SNo d) HmyS HmdS Htmp).
rewrite the current goal using (minus_SNo_invol d HdS) (from right to left) at position 1.
rewrite the current goal using (minus_SNo_invol (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) HyS) (from right to left) at position 1.
An exact proof term for the current goal is Htmp2.
An exact proof term for the current goal is (Hflip Hltneg).
We prove the intermediate claim HdltR: Rlt d (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b).
An exact proof term for the current goal is (RltI d (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) HdR HyR HdltY).
We prove the intermediate claim HyIn: apply_fun gdiv x ∈ open_ray_upper R d.
rewrite the current goal using (apply_fun_graph R (λx0 : set ⇒ div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) b) x HxR) (from left to right).
We prove the intermediate claim Hraydef: open_ray_upper R d = {t ∈ R|order_rel R d t}.
Use reflexivity.
rewrite the current goal using Hraydef (from left to right).
Apply SepI to the current goal.
An exact proof term for the current goal is HyR.
An exact proof term for the current goal is (Rlt_implies_order_rel_R d (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) HdltR).
An exact proof term for the current goal is (SepI R (λu : set ⇒ apply_fun gdiv u ∈ open_ray_upper R d) x HxR HyIn).
rewrite the current goal using HeqPre (from left to right).
We prove the intermediate claim HrayStd: open_ray_upper R x0 ∈ R_standard_topology.
We prove the intermediate claim HrInS: open_ray_upper R x0 ∈ S.
An exact proof term for the current goal is (open_ray_upper_in_open_rays_subbasis R x0 Hx0R).
We prove the intermediate claim HrGen: open_ray_upper R x0 ∈ generated_topology_from_subbasis R S.
An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis R S (open_ray_upper R x0) HS HrInS).
rewrite the current goal using Hgen (from right to left).
An exact proof term for the current goal is HrGen.
An exact proof term for the current goal is (HincStd (open_ray_upper R x0) HrayStd).
We prove the intermediate claim Hpre_lower: ∀d : set, d ∈ R → preimage_of R gdiv (open_ray_lower R d) ∈ Tx.
Let d be given.
Assume HdR: d ∈ R.
Apply (xm (a = 0)) to the current goal.
Assume Ha0: a = 0.
Set y0 to be the term div_SNo c b.
We prove the intermediate claim Hy0R: y0 ∈ R.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
We prove the intermediate claim HbReal: b ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HbR.
We prove the intermediate claim HcReal: c ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HcR.
We prove the intermediate claim Hy0Real: y0 ∈ real.
An exact proof term for the current goal is (real_div_SNo c HcReal b HbReal).
rewrite the current goal using HdefR (from left to right).
An exact proof term for the current goal is Hy0Real.
We prove the intermediate claim Hgapply: ∀x : set, x ∈ R → apply_fun gdiv x = y0.
Let x be given.
Assume HxR: x ∈ R.
rewrite the current goal using (apply_fun_graph R (λx0 : set ⇒ div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) b) x HxR) (from left to right).
rewrite the current goal using Ha0 (from left to right).
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
We prove the intermediate claim HxReal: x ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HxR.
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxReal).
We prove the intermediate claim HcReal: c ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HcR.
We prove the intermediate claim HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcReal).
rewrite the current goal using (mul_SNo_zeroL x HxS) (from left to right).
rewrite the current goal using (minus_SNo_0) (from left to right) at position 1.
rewrite the current goal using (add_SNo_0R c HcS) (from left to right) at position 1.
Use reflexivity.
Apply (xm (Rlt y0 d)) to the current goal.
Assume Hlt: Rlt y0 d.
We prove the intermediate claim HeqPre: preimage_of R gdiv (open_ray_lower R d) = R.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ preimage_of R gdiv (open_ray_lower R d).
An exact proof term for the current goal is (SepE1 R (λu : set ⇒ apply_fun gdiv u ∈ open_ray_lower R d) x Hx).
Let x be given.
Assume HxR: x ∈ R.
We will prove x ∈ preimage_of R gdiv (open_ray_lower R d).
We prove the intermediate claim HyIn: apply_fun gdiv x ∈ open_ray_lower R d.
rewrite the current goal using (Hgapply x HxR) (from left to right).
We prove the intermediate claim Hraydef: open_ray_lower R d = {t ∈ R|order_rel R t d}.
Use reflexivity.
rewrite the current goal using Hraydef (from left to right).
Apply SepI to the current goal.
An exact proof term for the current goal is Hy0R.
An exact proof term for the current goal is (Rlt_implies_order_rel_R y0 d Hlt).
An exact proof term for the current goal is (SepI R (λu : set ⇒ apply_fun gdiv u ∈ open_ray_lower R d) x HxR HyIn).
rewrite the current goal using HeqPre (from left to right).
An exact proof term for the current goal is (topology_has_X R Tx HTx).
Assume Hnlt: ¬ (Rlt y0 d).
We prove the intermediate claim HeqPre: preimage_of R gdiv (open_ray_lower R d) = Empty.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ preimage_of R gdiv (open_ray_lower R d).
Apply FalseE to the current goal.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λu : set ⇒ apply_fun gdiv u ∈ open_ray_lower R d) x Hx).
We prove the intermediate claim Himg: apply_fun gdiv x ∈ open_ray_lower R d.
An exact proof term for the current goal is (SepE2 R (λu : set ⇒ apply_fun gdiv u ∈ open_ray_lower R d) x Hx).
We prove the intermediate claim Hrel: order_rel R (apply_fun gdiv x) d.
An exact proof term for the current goal is (SepE2 R (λy : set ⇒ order_rel R y d) (apply_fun gdiv x) Himg).
We prove the intermediate claim Hlt: Rlt (apply_fun gdiv x) d.
An exact proof term for the current goal is (order_rel_R_implies_Rlt (apply_fun gdiv x) d Hrel).
We prove the intermediate claim HyEq: apply_fun gdiv x = y0.
An exact proof term for the current goal is (Hgapply x HxR).
We prove the intermediate claim Hlt2: Rlt y0 d.
rewrite the current goal using HyEq (from right to left).
An exact proof term for the current goal is Hlt.
An exact proof term for the current goal is (Hnlt Hlt2).
Let x be given.
Assume HxE: x ∈ Empty.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE x HxE).
rewrite the current goal using HeqPre (from left to right).
An exact proof term for the current goal is (topology_has_empty R Tx HTx).
Assume Ha0: ¬ (a = 0).
Set rhs to be the term add_SNo c (minus_SNo (mul_SNo b d)).
Set x0 to be the term div_SNo rhs a.
We prove the intermediate claim Hx0R: x0 ∈ R.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
We prove the intermediate claim Har: a ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HaR.
We prove the intermediate claim Hbr: b ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HbR.
We prove the intermediate claim Hcr: c ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HcR.
We prove the intermediate claim Hdr: d ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HdR.
We prove the intermediate claim Hrhr: rhs ∈ real.
An exact proof term for the current goal is (real_add_SNo c Hcr (minus_SNo (mul_SNo b d)) (real_minus_SNo (mul_SNo b d) (real_mul_SNo b Hbr d Hdr))).
We prove the intermediate claim Hx0r: x0 ∈ real.
An exact proof term for the current goal is (real_div_SNo rhs Hrhr a Har).
rewrite the current goal using HdefR (from left to right).
An exact proof term for the current goal is Hx0r.
We prove the intermediate claim Hyx0eq: div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) b = d.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
We prove the intermediate claim Har: a ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HaR.
We prove the intermediate claim Hbr: b ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HbR.
We prove the intermediate claim Hcr: c ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HcR.
We prove the intermediate claim Hdr: d ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HdR.
We prove the intermediate claim Hx0r: x0 ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is Hx0R.
We prove the intermediate claim Hrhr: rhs ∈ real.
rewrite the current goal using HdefR (from right to left).
We prove the intermediate claim HbrR: b ∈ R.
An exact proof term for the current goal is HbR.
We prove the intermediate claim HdrR: d ∈ R.
An exact proof term for the current goal is HdR.
We prove the intermediate claim HmulR: mul_SNo b d ∈ R.
An exact proof term for the current goal is (real_mul_SNo b HbR d HdR).
We prove the intermediate claim HmR: minus_SNo (mul_SNo b d) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (mul_SNo b d) HmulR).
An exact proof term for the current goal is (real_add_SNo c HcR (minus_SNo (mul_SNo b d)) HmR).
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 HcS: SNo c.
An exact proof term for the current goal is (real_SNo c Hcr).
We prove the intermediate claim HdS: SNo d.
An exact proof term for the current goal is (real_SNo d Hdr).
We prove the intermediate claim HrhsS: SNo rhs.
An exact proof term for the current goal is (SNo_add_SNo c (minus_SNo (mul_SNo b d)) HcS (SNo_minus_SNo (mul_SNo b d) (SNo_mul_SNo b d HbS HdS))).
We prove the intermediate claim Ha0': a ≠ 0.
Assume Ha0eq: a = 0.
An exact proof term for the current goal is (Ha0 Ha0eq).
We prove the intermediate claim Hmulax0: mul_SNo a x0 = rhs.
rewrite the current goal using (mul_div_SNo_invR rhs a HrhsS HaS Ha0') (from left to right).
Use reflexivity.
We prove the intermediate claim HnumEq: add_SNo c (minus_SNo (mul_SNo a x0)) = mul_SNo b d.
rewrite the current goal using Hmulax0 (from left to right).
We prove the intermediate claim Hneg: minus_SNo rhs = add_SNo (minus_SNo c) (minus_SNo (minus_SNo (mul_SNo b d))).
An exact proof term for the current goal is (minus_add_SNo_distr c (minus_SNo (mul_SNo b d)) HcS (SNo_minus_SNo (mul_SNo b d) (SNo_mul_SNo b d HbS HdS))).
We prove the intermediate claim Hinv: minus_SNo (minus_SNo (mul_SNo b d)) = mul_SNo b d.
An exact proof term for the current goal is (minus_SNo_invol (mul_SNo b d) (SNo_mul_SNo b d HbS HdS)).
rewrite the current goal using Hneg (from left to right).
rewrite the current goal using Hinv (from left to right) at position 1.
rewrite the current goal using (add_SNo_assoc c (minus_SNo c) (mul_SNo b d) HcS (SNo_minus_SNo c HcS) (SNo_mul_SNo b d HbS HdS)) (from left to right).
rewrite the current goal using (add_SNo_minus_SNo_rinv c HcS) (from left to right) at position 1.
rewrite the current goal using (add_SNo_0L (mul_SNo b d) (SNo_mul_SNo b d HbS HdS)) (from left to right).
Use reflexivity.
rewrite the current goal using HnumEq (from left to right).
Apply (mul_div_SNo_nonzero_eq (mul_SNo b d) b d (SNo_mul_SNo b d HbS HdS) HbS HdS Hbne) to the current goal.
Use reflexivity.
We prove the intermediate claim Hgdiv_x0: apply_fun gdiv x0 = d.
rewrite the current goal using (apply_fun_graph R (λx0 : set ⇒ div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) b) x0 Hx0R) (from left to right).
rewrite the current goal using Hyx0eq (from left to right).
Use reflexivity.
Set Pre to be the term preimage_of R gdiv (open_ray_lower R d).
Apply (xm (same_sign_nonzero_R a b)) to the current goal.
Assume Hsign: same_sign_nonzero_R a b.
We prove the intermediate claim HeqPre: Pre = open_ray_upper R x0.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ Pre.
We will prove x ∈ open_ray_upper R x0.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λu : set ⇒ apply_fun gdiv u ∈ open_ray_lower R d) x Hx).
We prove the intermediate claim Himg: apply_fun gdiv x ∈ open_ray_lower R d.
An exact proof term for the current goal is (SepE2 R (λu : set ⇒ apply_fun gdiv u ∈ open_ray_lower R d) x Hx).
We prove the intermediate claim Hrel: order_rel R (apply_fun gdiv x) d.
An exact proof term for the current goal is (SepE2 R (λy : set ⇒ order_rel R y d) (apply_fun gdiv x) Himg).
We prove the intermediate claim Hylt: Rlt (apply_fun gdiv x) d.
An exact proof term for the current goal is (order_rel_R_implies_Rlt (apply_fun gdiv x) d Hrel).
We prove the intermediate claim Hylt2: Rlt (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) d.
rewrite the current goal using (apply_fun_graph R (λx0 : set ⇒ div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) b) x HxR) (from right to left).
An exact proof term for the current goal is Hylt.
We prove the intermediate claim HxReal: x ∈ real.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HxR.
We prove the intermediate claim Hx0Real: x0 ∈ real.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is Hx0R.
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxReal).
We prove the intermediate claim Hx0S: SNo x0.
An exact proof term for the current goal is (real_SNo x0 Hx0Real).
Apply (SNoLt_trichotomy_or_impred x x0 HxS Hx0S (x ∈ open_ray_upper R x0)) to the current goal.
Assume Hxlt: x < x0.
Apply FalseE to the current goal.
We prove the intermediate claim HxltR: Rlt x x0.
An exact proof term for the current goal is (RltI x x0 HxR Hx0R Hxlt).
We prove the intermediate claim Hdec: Rlt (div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) b) (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b).
An exact proof term for the current goal is (affine_line_R2_param_by_x_y_decreases_same_sign a b c x x0 HaR HbR HcR Hbne Hsign HxR Hx0R HxltR).
We prove the intermediate claim Hdlt0: Rlt d (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b).
rewrite the current goal using Hyx0eq (from right to left) at position 1.
An exact proof term for the current goal is Hdec.
An exact proof term for the current goal is (not_Rlt_sym (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) d Hylt2 Hdlt0).
Assume Hxeq: x = x0.
Apply FalseE to the current goal.
We prove the intermediate claim Hylt0: Rlt (apply_fun gdiv x0) d.
rewrite the current goal using Hxeq (from right to left).
An exact proof term for the current goal is Hylt.
We prove the intermediate claim Hdltdd: Rlt d d.
rewrite the current goal using Hgdiv_x0 (from right to left) at position 1.
An exact proof term for the current goal is Hylt0.
An exact proof term for the current goal is (not_Rlt_refl d HdR Hdltdd).
Assume Hx0lt: x0 < x.
We prove the intermediate claim Hx0ltR: Rlt x0 x.
An exact proof term for the current goal is (RltI x0 x Hx0R HxR Hx0lt).
We prove the intermediate claim Hraydef: open_ray_upper R x0 = {t ∈ R|order_rel R x0 t}.
Use reflexivity.
rewrite the current goal using Hraydef (from left to right).
Apply SepI to the current goal.
An exact proof term for the current goal is HxR.
An exact proof term for the current goal is (Rlt_implies_order_rel_R x0 x Hx0ltR).
Let x be given.
Assume Hx: x ∈ open_ray_upper R x0.
We will prove x ∈ Pre.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λu : set ⇒ order_rel R x0 u) x Hx).
We prove the intermediate claim Hrel: order_rel R x0 x.
An exact proof term for the current goal is (SepE2 R (λu : set ⇒ order_rel R x0 u) x Hx).
We prove the intermediate claim Hx0ltR: Rlt x0 x.
An exact proof term for the current goal is (order_rel_R_implies_Rlt x0 x Hrel).
We prove the intermediate claim Hdec: Rlt (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) (div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) b).
An exact proof term for the current goal is (affine_line_R2_param_by_x_y_decreases_same_sign a b c x0 x HaR HbR HcR Hbne Hsign Hx0R HxR Hx0ltR).
We prove the intermediate claim HyIn: apply_fun gdiv x ∈ open_ray_lower R d.
rewrite the current goal using (apply_fun_graph R (λx0 : set ⇒ div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) b) x HxR) (from left to right).
We prove the intermediate claim Hraydef: open_ray_lower R d = {t ∈ R|order_rel R t d}.
Use reflexivity.
rewrite the current goal using Hraydef (from left to right).
Apply SepI to the current goal.
An exact proof term for the current goal is (real_div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) (real_add_SNo c HcR (minus_SNo (mul_SNo a x)) (real_minus_SNo (mul_SNo a x) (real_mul_SNo a HaR x HxR))) b HbR).
We prove the intermediate claim Hyltd: Rlt (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) d.
rewrite the current goal using Hyx0eq (from right to left).
An exact proof term for the current goal is Hdec.
An exact proof term for the current goal is (Rlt_implies_order_rel_R (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) d Hyltd).
An exact proof term for the current goal is (SepI R (λu : set ⇒ apply_fun gdiv u ∈ open_ray_lower R d) x HxR HyIn).
rewrite the current goal using HeqPre (from left to right).
We prove the intermediate claim HrayStd: open_ray_upper R x0 ∈ R_standard_topology.
We prove the intermediate claim HrInS: open_ray_upper R x0 ∈ S.
An exact proof term for the current goal is (open_ray_upper_in_open_rays_subbasis R x0 Hx0R).
We prove the intermediate claim HrGen: open_ray_upper R x0 ∈ generated_topology_from_subbasis R S.
An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis R S (open_ray_upper R x0) HS HrInS).
rewrite the current goal using Hgen (from right to left).
An exact proof term for the current goal is HrGen.
An exact proof term for the current goal is (HincStd (open_ray_upper R x0) HrayStd).
Assume Hnotsign: ¬ (same_sign_nonzero_R a b).
Set mb to be the term minus_SNo b.
We prove the intermediate claim HmbR: mb ∈ R.
An exact proof term for the current goal is (real_minus_SNo b HbR).
We prove the intermediate claim Hmb0: mb ≠ 0.
Assume Hmb0eq: mb = 0.
We prove the intermediate claim Hb0eq: b = 0.
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 Hmbdef: mb = minus_SNo b.
Use reflexivity.
rewrite the current goal using (minus_SNo_invol b HbS) (from right to left) at position 1.
rewrite the current goal using Hmbdef (from right to left) at position 1.
rewrite the current goal using Hmb0eq (from left to right).
rewrite the current goal using minus_SNo_0 (from left to right).
Use reflexivity.
An exact proof term for the current goal is (Hbne Hb0eq).
We prove the intermediate claim Hsignmb: same_sign_nonzero_R a mb.
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).
Apply (SNoLt_trichotomy_or_impred a 0 HaS SNo_0 (same_sign_nonzero_R a mb)) to the current goal.
Assume Halt0: a < 0.
Apply (SNoLt_trichotomy_or_impred b 0 HbS SNo_0 (same_sign_nonzero_R a mb)) to the current goal.
Assume Hblt0: b < 0.
Apply FalseE to the current goal.
We prove the intermediate claim Halt0R: Rlt a 0.
An exact proof term for the current goal is (RltI a 0 HaR real_0 Halt0).
We prove the intermediate claim Hblt0R: Rlt b 0.
An exact proof term for the current goal is (RltI b 0 HbR real_0 Hblt0).
We prove the intermediate claim Hss: same_sign_nonzero_R a b.
An exact proof term for the current goal is (orIR (Rlt 0 a ∧ Rlt 0 b) (Rlt a 0 ∧ Rlt b 0) (andI (Rlt a 0) (Rlt b 0) Halt0R Hblt0R)).
An exact proof term for the current goal is (Hnotsign Hss).
Assume Hb0eq: b = 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hbne Hb0eq).
Assume H0blt: 0 < b.
We prove the intermediate claim Halt0R: Rlt a 0.
An exact proof term for the current goal is (RltI a 0 HaR real_0 Halt0).
We prove the intermediate claim HmbS: SNo mb.
An exact proof term for the current goal is (SNo_minus_SNo b HbS).
We prove the intermediate claim Hmblt0: mb < 0.
We prove the intermediate claim Hflip: minus_SNo b < minus_SNo 0.
An exact proof term for the current goal is (minus_SNo_Lt_contra 0 b SNo_0 HbS H0blt).
rewrite the current goal using (minus_SNo_0) (from right to left) at position 1.
An exact proof term for the current goal is Hflip.
We prove the intermediate claim HmbLt0R: Rlt mb 0.
An exact proof term for the current goal is (RltI mb 0 HmbR real_0 Hmblt0).
An exact proof term for the current goal is (orIR (Rlt 0 a ∧ Rlt 0 mb) (Rlt a 0 ∧ Rlt mb 0) (andI (Rlt a 0) (Rlt mb 0) Halt0R HmbLt0R)).
Assume Ha0eq: a = 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Ha0 Ha0eq).
Assume H0alt: 0 < a.
Apply (SNoLt_trichotomy_or_impred b 0 HbS SNo_0 (same_sign_nonzero_R a mb)) to the current goal.
Assume Hblt0: b < 0.
We prove the intermediate claim H0aR: Rlt 0 a.
An exact proof term for the current goal is (RltI 0 a real_0 HaR H0alt).
We prove the intermediate claim HmbS: SNo mb.
An exact proof term for the current goal is (SNo_minus_SNo b HbS).
We prove the intermediate claim H0mblt: 0 < mb.
We prove the intermediate claim Hflip: minus_SNo 0 < minus_SNo b.
An exact proof term for the current goal is (minus_SNo_Lt_contra b 0 HbS SNo_0 Hblt0).
rewrite the current goal using (minus_SNo_0) (from right to left) at position 1.
An exact proof term for the current goal is Hflip.
We prove the intermediate claim H0mbR: Rlt 0 mb.
An exact proof term for the current goal is (RltI 0 mb real_0 HmbR H0mblt).
An exact proof term for the current goal is (orIL (Rlt 0 a ∧ Rlt 0 mb) (Rlt a 0 ∧ Rlt mb 0) (andI (Rlt 0 a) (Rlt 0 mb) H0aR H0mbR)).
Assume Hb0eq: b = 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hbne Hb0eq).
Assume H0blt: 0 < b.
Apply FalseE to the current goal.
We prove the intermediate claim H0aR: Rlt 0 a.
An exact proof term for the current goal is (RltI 0 a real_0 HaR H0alt).
We prove the intermediate claim H0bR: Rlt 0 b.
An exact proof term for the current goal is (RltI 0 b real_0 HbR H0blt).
We prove the intermediate claim Hss: same_sign_nonzero_R a b.
An exact proof term for the current goal is (orIL (Rlt 0 a ∧ Rlt 0 b) (Rlt a 0 ∧ Rlt b 0) (andI (Rlt 0 a) (Rlt 0 b) H0aR H0bR)).
An exact proof term for the current goal is (Hnotsign Hss).
We prove the intermediate claim HdivMinusDen: ∀t : set, t ∈ R → div_SNo t mb = minus_SNo (div_SNo t b).
Let t be given.
Assume HtR: t ∈ R.
We prove the intermediate claim HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim Hmbdef: mb = minus_SNo b.
Use reflexivity.
rewrite the current goal using Hmbdef (from left to right).
We prove the intermediate claim Hrecip: recip_SNo (minus_SNo b) = minus_SNo (recip_SNo b).
Apply (SNoLt_trichotomy_or_impred b 0 HbS SNo_0 (recip_SNo (minus_SNo b) = minus_SNo (recip_SNo b))) to the current goal.
Assume Hblt0: b < 0.
We prove the intermediate claim HmbS: SNo (minus_SNo b).
An exact proof term for the current goal is (SNo_minus_SNo b HbS).
We prove the intermediate claim H0mb: 0 < minus_SNo b.
We prove the intermediate claim Htmp: minus_SNo 0 < minus_SNo b.
An exact proof term for the current goal is (minus_SNo_Lt_contra b 0 HbS SNo_0 Hblt0).
rewrite the current goal using (minus_SNo_0) (from right to left) at position 1.
An exact proof term for the current goal is Htmp.
rewrite the current goal using (recip_SNo_poscase (minus_SNo b) H0mb) (from left to right).
rewrite the current goal using (recip_SNo_negcase b HbS Hblt0) (from left to right).
We prove the intermediate claim HtPosS: SNo (recip_SNo_pos (minus_SNo b)).
An exact proof term for the current goal is (SNo_recip_SNo_pos (minus_SNo b) HmbS H0mb).
rewrite the current goal using (minus_SNo_invol (recip_SNo_pos (minus_SNo b)) HtPosS) (from left to right).
Use reflexivity.
Assume Hb0eq: b = 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hbne Hb0eq).
Assume H0blt: 0 < b.
We prove the intermediate claim HmbS: SNo (minus_SNo b).
An exact proof term for the current goal is (SNo_minus_SNo b HbS).
We prove the intermediate claim Hmblt0: minus_SNo b < 0.
We prove the intermediate claim Htmp: minus_SNo b < minus_SNo 0.
An exact proof term for the current goal is (minus_SNo_Lt_contra 0 b SNo_0 HbS H0blt).
rewrite the current goal using (minus_SNo_0) (from right to left) at position 1.
An exact proof term for the current goal is Htmp.
rewrite the current goal using (recip_SNo_negcase (minus_SNo b) HmbS Hmblt0) (from left to right).
rewrite the current goal using (minus_SNo_invol b HbS) (from left to right) at position 1.
rewrite the current goal using (recip_SNo_poscase b H0blt) (from left to right).
Use reflexivity.
We prove the intermediate claim Hdivdef1: div_SNo t (minus_SNo b) = mul_SNo t (recip_SNo (minus_SNo b)).
Use reflexivity.
We prove the intermediate claim Hdivdef2: div_SNo t b = mul_SNo t (recip_SNo b).
Use reflexivity.
rewrite the current goal using Hdivdef1 (from left to right).
rewrite the current goal using Hdivdef2 (from left to right).
rewrite the current goal using Hrecip (from left to right).
An exact proof term for the current goal is (mul_SNo_minus_distrR t (recip_SNo b) HtS (SNo_recip_SNo b HbS)).
We prove the intermediate claim HeqPre: Pre = open_ray_lower R x0.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ Pre.
We will prove x ∈ open_ray_lower R x0.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λu : set ⇒ apply_fun gdiv u ∈ open_ray_lower R d) x Hx).
We prove the intermediate claim Himg: apply_fun gdiv x ∈ open_ray_lower R d.
An exact proof term for the current goal is (SepE2 R (λu : set ⇒ apply_fun gdiv u ∈ open_ray_lower R d) x Hx).
We prove the intermediate claim Hrel: order_rel R (apply_fun gdiv x) d.
An exact proof term for the current goal is (SepE2 R (λy : set ⇒ order_rel R y d) (apply_fun gdiv x) Himg).
We prove the intermediate claim Hylt: Rlt (apply_fun gdiv x) d.
An exact proof term for the current goal is (order_rel_R_implies_Rlt (apply_fun gdiv x) d Hrel).
We prove the intermediate claim Hylt2: Rlt (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) d.
rewrite the current goal using (apply_fun_graph R (λx0 : set ⇒ div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) b) x HxR) (from right to left) at position 1.
An exact proof term for the current goal is Hylt.
We prove the intermediate claim HxReal: x ∈ real.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HxR.
We prove the intermediate claim Hx0Real: x0 ∈ real.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is Hx0R.
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxReal).
We prove the intermediate claim Hx0S: SNo x0.
An exact proof term for the current goal is (real_SNo x0 Hx0Real).
Apply (SNoLt_trichotomy_or_impred x x0 HxS Hx0S (x ∈ open_ray_lower R x0)) to the current goal.
Assume Hxlt: x < x0.
We prove the intermediate claim HxltR: Rlt x x0.
An exact proof term for the current goal is (RltI x x0 HxR Hx0R Hxlt).
We prove the intermediate claim Hraydef: open_ray_lower R x0 = {t ∈ R|order_rel R t x0}.
Use reflexivity.
rewrite the current goal using Hraydef (from left to right).
Apply SepI to the current goal.
An exact proof term for the current goal is HxR.
An exact proof term for the current goal is (Rlt_implies_order_rel_R x x0 HxltR).
Assume Hxeq: x = x0.
Apply FalseE to the current goal.
We prove the intermediate claim Hylt0: Rlt (apply_fun gdiv x0) d.
rewrite the current goal using Hxeq (from right to left).
An exact proof term for the current goal is Hylt.
We prove the intermediate claim Hdltdd: Rlt d d.
rewrite the current goal using Hgdiv_x0 (from right to left) at position 1.
An exact proof term for the current goal is Hylt0.
An exact proof term for the current goal is (not_Rlt_refl d HdR Hdltdd).
Assume Hx0lt: x0 < x.
Apply FalseE to the current goal.
We prove the intermediate claim Hx0ltR: Rlt x0 x.
An exact proof term for the current goal is (RltI x0 x Hx0R HxR Hx0lt).
We prove the intermediate claim HdecNeg: Rlt (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) mb) (div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) mb).
An exact proof term for the current goal is (affine_line_R2_param_by_x_y_decreases_same_sign a mb c x0 x HaR HmbR HcR Hmb0 Hsignmb Hx0R HxR Hx0ltR).
We prove the intermediate claim HnumxR: add_SNo c (minus_SNo (mul_SNo a x)) ∈ R.
We prove the intermediate claim HaxR: mul_SNo a x ∈ R.
An exact proof term for the current goal is (real_mul_SNo a HaR x HxR).
We prove the intermediate claim HmxR: minus_SNo (mul_SNo a x) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (mul_SNo a x) HaxR).
An exact proof term for the current goal is (real_add_SNo c HcR (minus_SNo (mul_SNo a x)) HmxR).
We prove the intermediate claim Hnumx0R: add_SNo c (minus_SNo (mul_SNo a x0)) ∈ R.
We prove the intermediate claim Hax0R2: mul_SNo a x0 ∈ R.
An exact proof term for the current goal is (real_mul_SNo a HaR x0 Hx0R).
We prove the intermediate claim Hmx0R: minus_SNo (mul_SNo a x0) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (mul_SNo a x0) Hax0R2).
An exact proof term for the current goal is (real_add_SNo c HcR (minus_SNo (mul_SNo a x0)) Hmx0R).
We prove the intermediate claim Hynegx: div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) mb = minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b).
An exact proof term for the current goal is (HdivMinusDen (add_SNo c (minus_SNo (mul_SNo a x))) HnumxR).
We prove the intermediate claim Hynegx0: div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) mb = minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) b).
An exact proof term for the current goal is (HdivMinusDen (add_SNo c (minus_SNo (mul_SNo a x0))) Hnumx0R).
We prove the intermediate claim Hltneg: Rlt (div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) mb) (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) mb).
We prove the intermediate claim HyR: div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b ∈ R.
An exact proof term for the current goal is (RltE_left (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) d Hylt2).
We prove the intermediate claim HdS: SNo d.
An exact proof term for the current goal is (real_SNo d HdR).
We prove the intermediate claim HyS: SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b).
An exact proof term for the current goal is (real_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) HyR).
We prove the intermediate claim HyltS: div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b < d.
An exact proof term for the current goal is (RltE_lt (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) d Hylt2).
We prove the intermediate claim HltnegS: minus_SNo d < minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b).
An exact proof term for the current goal is (minus_SNo_Lt_contra (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) d HyS HdS HyltS).
We prove the intermediate claim HmdR: minus_SNo d ∈ R.
An exact proof term for the current goal is (real_minus_SNo d HdR).
We prove the intermediate claim HmyR: minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) HyR).
We prove the intermediate claim HltnegR: Rlt (minus_SNo d) (minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b)).
An exact proof term for the current goal is (RltI (minus_SNo d) (minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b)) HmdR HmyR HltnegS).
rewrite the current goal using Hynegx0 (from left to right) at position 1.
rewrite the current goal using Hyx0eq (from left to right) at position 1.
rewrite the current goal using Hynegx (from left to right).
An exact proof term for the current goal is HltnegR.
An exact proof term for the current goal is ((not_Rlt_sym (div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) mb) (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) mb) Hltneg) HdecNeg).
Let x be given.
Assume Hx: x ∈ open_ray_lower R x0.
We will prove x ∈ Pre.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λu : set ⇒ order_rel R u x0) x Hx).
We prove the intermediate claim Hrel: order_rel R x x0.
An exact proof term for the current goal is (SepE2 R (λu : set ⇒ order_rel R u x0) x Hx).
We prove the intermediate claim HxltR: Rlt x x0.
An exact proof term for the current goal is (order_rel_R_implies_Rlt x x0 Hrel).
We prove the intermediate claim HdecNeg: Rlt (div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) mb) (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) mb).
An exact proof term for the current goal is (affine_line_R2_param_by_x_y_decreases_same_sign a mb c x x0 HaR HmbR HcR Hmb0 Hsignmb HxR Hx0R HxltR).
We prove the intermediate claim HnumxR: add_SNo c (minus_SNo (mul_SNo a x)) ∈ R.
We prove the intermediate claim HaxR: mul_SNo a x ∈ R.
An exact proof term for the current goal is (real_mul_SNo a HaR x HxR).
We prove the intermediate claim HmxR: minus_SNo (mul_SNo a x) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (mul_SNo a x) HaxR).
An exact proof term for the current goal is (real_add_SNo c HcR (minus_SNo (mul_SNo a x)) HmxR).
We prove the intermediate claim Hnumx0R: add_SNo c (minus_SNo (mul_SNo a x0)) ∈ R.
We prove the intermediate claim Hax0R2: mul_SNo a x0 ∈ R.
An exact proof term for the current goal is (real_mul_SNo a HaR x0 Hx0R).
We prove the intermediate claim Hmx0R: minus_SNo (mul_SNo a x0) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (mul_SNo a x0) Hax0R2).
An exact proof term for the current goal is (real_add_SNo c HcR (minus_SNo (mul_SNo a x0)) Hmx0R).
We prove the intermediate claim Hynegx: div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) mb = minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b).
An exact proof term for the current goal is (HdivMinusDen (add_SNo c (minus_SNo (mul_SNo a x))) HnumxR).
We prove the intermediate claim Hynegx0: div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) mb = minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) b).
An exact proof term for the current goal is (HdivMinusDen (add_SNo c (minus_SNo (mul_SNo a x0))) Hnumx0R).
We prove the intermediate claim HyR: div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b ∈ R.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
We prove the intermediate claim HbReal: b ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HbR.
We prove the intermediate claim HnumReal: add_SNo c (minus_SNo (mul_SNo a x)) ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HnumxR.
We prove the intermediate claim HyReal: div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b ∈ real.
An exact proof term for the current goal is (real_div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) HnumReal b HbReal).
rewrite the current goal using HdefR (from left to right).
An exact proof term for the current goal is HyReal.
We prove the intermediate claim HdS: SNo d.
An exact proof term for the current goal is (real_SNo d HdR).
We prove the intermediate claim HyS: SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b).
An exact proof term for the current goal is (real_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) HyR).
We prove the intermediate claim HltnegS: minus_SNo d < minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b).
We prove the intermediate claim Htmp: div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) mb < div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) mb.
An exact proof term for the current goal is (RltE_lt (div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) mb) (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) mb) HdecNeg).
rewrite the current goal using Hyx0eq (from right to left) at position 1.
rewrite the current goal using Hynegx0 (from right to left) at position 1.
rewrite the current goal using Hynegx (from right to left).
An exact proof term for the current goal is Htmp.
We prove the intermediate claim HyltS: div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b < d.
We prove the intermediate claim HmdS: SNo (minus_SNo d).
An exact proof term for the current goal is (SNo_minus_SNo d HdS).
We prove the intermediate claim HmyS: SNo (minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b)).
An exact proof term for the current goal is (SNo_minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) HyS).
We prove the intermediate claim Htmp: minus_SNo (minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b)) < minus_SNo (minus_SNo d).
An exact proof term for the current goal is (minus_SNo_Lt_contra (minus_SNo d) (minus_SNo (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b)) HmdS HmyS HltnegS).
rewrite the current goal using (minus_SNo_invol (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) HyS) (from right to left) at position 1.
rewrite the current goal using (minus_SNo_invol d HdS) (from right to left) at position 1.
An exact proof term for the current goal is Htmp.
We prove the intermediate claim HyltR: Rlt (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) d.
An exact proof term for the current goal is (RltI (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) d HyR HdR HyltS).
We prove the intermediate claim HyIn: apply_fun gdiv x ∈ open_ray_lower R d.
rewrite the current goal using (apply_fun_graph R (λx0 : set ⇒ div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) b) x HxR) (from left to right).
We prove the intermediate claim Hraydef: open_ray_lower R d = {t ∈ R|order_rel R t d}.
Use reflexivity.
rewrite the current goal using Hraydef (from left to right).
Apply SepI to the current goal.
An exact proof term for the current goal is HyR.
An exact proof term for the current goal is (Rlt_implies_order_rel_R (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) d HyltR).
An exact proof term for the current goal is (SepI R (λu : set ⇒ apply_fun gdiv u ∈ open_ray_lower R d) x HxR HyIn).
rewrite the current goal using HeqPre (from left to right).
We prove the intermediate claim HrayStd: open_ray_lower R x0 ∈ R_standard_topology.
We prove the intermediate claim HrInS: open_ray_lower R x0 ∈ S.
An exact proof term for the current goal is (open_ray_lower_in_open_rays_subbasis R x0 Hx0R).
We prove the intermediate claim HrGen: open_ray_lower R x0 ∈ generated_topology_from_subbasis R S.
An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis R S (open_ray_lower R x0) HS HrInS).
rewrite the current goal using Hgen (from right to left).
An exact proof term for the current goal is HrGen.
An exact proof term for the current goal is (HincStd (open_ray_lower R x0) HrayStd).
rewrite the current goal using Hgen (from right to left).
Apply (continuous_map_from_subbasis R Tx R S gdiv HTx Hfun HS) to the current goal.
Let s be given.
Assume HsS: s ∈ S.
We will prove preimage_of R gdiv s ∈ Tx.
Apply (binunionE' ({I ∈ 𝒫 R|∃a0 ∈ R, I = open_ray_upper R a0} ∪ {I ∈ 𝒫 R|∃b0 ∈ R, I = open_ray_lower R b0}) {R} s (preimage_of R gdiv s ∈ Tx)) to the current goal.
Assume Hs0: s ∈ ({I ∈ 𝒫 R|∃a0 ∈ R, I = open_ray_upper R a0} ∪ {I ∈ 𝒫 R|∃b0 ∈ R, I = open_ray_lower R b0}).
Apply (binunionE' {I ∈ 𝒫 R|∃a0 ∈ R, I = open_ray_upper R a0} {I ∈ 𝒫 R|∃b0 ∈ R, I = open_ray_lower R b0} s (preimage_of R gdiv s ∈ Tx)) to the current goal.
Assume HsU: s ∈ {I ∈ 𝒫 R|∃a0 ∈ R, I = open_ray_upper R a0}.
We prove the intermediate claim Hexa: ∃d ∈ R, s = open_ray_upper R d.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λI0 : set ⇒ ∃a0 ∈ R, I0 = open_ray_upper R a0) s HsU).
Apply Hexa to the current goal.
Let d be given.
Assume HdPair.
We prove the intermediate claim HdR: d ∈ R.
An exact proof term for the current goal is (andEL (d ∈ R) (s = open_ray_upper R d) HdPair).
We prove the intermediate claim Hseq: s = open_ray_upper R d.
An exact proof term for the current goal is (andER (d ∈ R) (s = open_ray_upper R d) HdPair).
rewrite the current goal using Hseq (from left to right).
An exact proof term for the current goal is (Hpre_upper d HdR).
Assume HsL: s ∈ {I ∈ 𝒫 R|∃b0 ∈ R, I = open_ray_lower R b0}.
We prove the intermediate claim Hexb: ∃d ∈ R, s = open_ray_lower R d.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λI0 : set ⇒ ∃b0 ∈ R, I0 = open_ray_lower R b0) s HsL).
Apply Hexb to the current goal.
Let d be given.
Assume HdPair.
We prove the intermediate claim HdR: d ∈ R.
An exact proof term for the current goal is (andEL (d ∈ R) (s = open_ray_lower R d) HdPair).
We prove the intermediate claim Hseq: s = open_ray_lower R d.
An exact proof term for the current goal is (andER (d ∈ R) (s = open_ray_lower R d) HdPair).
rewrite the current goal using Hseq (from left to right).
An exact proof term for the current goal is (Hpre_lower d HdR).
An exact proof term for the current goal is Hs0.
Assume HsR: s ∈ {R}.
We prove the intermediate claim Hseq: s = R.
An exact proof term for the current goal is (SingE R s HsR).
rewrite the current goal using Hseq (from left to right).
rewrite the current goal using (preimage_of_whole R R gdiv 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.
∎