Let a be given.
Assume HaR: a ∈ R.
We will prove preimage_of (open_interval (minus_SNo 1) 1) bounded_transform_psi (open_ray_upper R a) ∈ subspace_topology R R_standard_topology (open_interval (minus_SNo 1) 1).
Set I to be the term open_interval (minus_SNo 1) 1.
Set U to be the term preimage_of I bounded_transform_psi (open_ray_upper R a).
We prove the intermediate claim HI_sub_R: I ⊆ R.
Let x be given.
Assume HxI: x ∈ I.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ Rlt (minus_SNo 1) x0 ∧ Rlt x0 1) x HxI).
Set c to be the term apply_fun bounded_transform_phi a.
We prove the intermediate claim HcR: c ∈ R.
An exact proof term for the current goal is (bounded_transform_phi_value_in_R a HaR).
We prove the intermediate claim HrayOpen: open_ray_upper R c ∈ R_standard_topology.
rewrite the current goal using standard_topology_is_order_topology (from right to left).
We prove the intermediate claim Hsub: open_ray_upper R c ∈ open_rays_subbasis R.
An exact proof term for the current goal is (open_ray_upper_in_open_rays_subbasis R c HcR).
An exact proof term for the current goal is (open_rays_subbasis_sub_order_topology_R (open_ray_upper R c) Hsub).
We prove the intermediate claim Heq: U = (open_ray_upper R c) ∩ I.
We prove the intermediate claim HUdef: U = preimage_of I bounded_transform_psi (open_ray_upper R a).
Use reflexivity.
We prove the intermediate claim Hpredef: preimage_of I bounded_transform_psi (open_ray_upper R a) = {x0 ∈ I|apply_fun bounded_transform_psi x0 ∈ open_ray_upper R a}.
Use reflexivity.
Apply set_ext to the current goal.
Let s be given.
Assume HsU: s ∈ U.
We will prove s ∈ (open_ray_upper R c) ∩ I.
We prove the intermediate claim HsU0: s ∈ preimage_of I bounded_transform_psi (open_ray_upper R a).
rewrite the current goal using HUdef (from right to left).
An exact proof term for the current goal is HsU.
We prove the intermediate claim HsU1: s ∈ {x0 ∈ I|apply_fun bounded_transform_psi x0 ∈ open_ray_upper R a}.
rewrite the current goal using Hpredef (from right to left).
An exact proof term for the current goal is HsU0.
We prove the intermediate claim HsI: s ∈ I.
An exact proof term for the current goal is (SepE1 I (λx0 : set ⇒ apply_fun bounded_transform_psi x0 ∈ open_ray_upper R a) s HsU1).
We prove the intermediate claim HsR: s ∈ R.
An exact proof term for the current goal is (HI_sub_R s HsI).
We prove the intermediate claim HpsiRay: apply_fun bounded_transform_psi s ∈ open_ray_upper R a.
An exact proof term for the current goal is (SepE2 I (λx0 : set ⇒ apply_fun bounded_transform_psi x0 ∈ open_ray_upper R a) s HsU1).
We prove the intermediate claim HpsiR: apply_fun bounded_transform_psi s ∈ R.
We prove the intermediate claim HabsR: abs_SNo s ∈ R.
An exact proof term for the current goal is (abs_SNo_in_R s HsR).
We prove the intermediate claim HminR: minus_SNo (abs_SNo s) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (abs_SNo s) HabsR).
We prove the intermediate claim HdenR: add_SNo 1 (minus_SNo (abs_SNo s)) ∈ R.
An exact proof term for the current goal is (real_add_SNo 1 real_1 (minus_SNo (abs_SNo s)) HminR).
We prove the intermediate claim HpsiDef: bounded_transform_psi = graph R (λs0 : set ⇒ div_SNo s0 (add_SNo 1 (minus_SNo (abs_SNo s0)))).
Use reflexivity.
rewrite the current goal using HpsiDef (from left to right).
rewrite the current goal using (apply_fun_graph R (λs0 : set ⇒ div_SNo s0 (add_SNo 1 (minus_SNo (abs_SNo s0)))) s HsR) (from left to right).
An exact proof term for the current goal is (real_div_SNo s HsR (add_SNo 1 (minus_SNo (abs_SNo s))) HdenR).
We prove the intermediate claim HrelA: order_rel R a (apply_fun bounded_transform_psi s).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R a x0) (apply_fun bounded_transform_psi s) HpsiRay).
We prove the intermediate claim HaltA: Rlt a (apply_fun bounded_transform_psi s).
An exact proof term for the current goal is (order_rel_R_implies_Rlt a (apply_fun bounded_transform_psi s) HrelA).
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 HsS: SNo s.
An exact proof term for the current goal is (real_SNo s HsR).
We prove the intermediate claim HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcR).
Apply (xm (Rlt a 0)) to the current goal.
Assume Halt0: Rlt a 0.
We prove the intermediate claim Halt0S: a < 0.
An exact proof term for the current goal is (RltE_lt a 0 Halt0).
Apply (xm (0 ≤ s)) to the current goal.
Assume H0les: 0 ≤ s.
We prove the intermediate claim HdenApos: 0 < add_SNo 1 (abs_SNo a).
We prove the intermediate claim HabsR: abs_SNo a ∈ R.
An exact proof term for the current goal is (abs_SNo_in_R a HaR).
We prove the intermediate claim HabsS: SNo (abs_SNo a).
An exact proof term for the current goal is (real_SNo (abs_SNo a) HabsR).
We prove the intermediate claim H0le_abs: 0 ≤ abs_SNo a.
An exact proof term for the current goal is (abs_SNo_nonneg a HaS).
We prove the intermediate claim HdenPos0: add_SNo 0 0 < add_SNo 1 (abs_SNo a).
An exact proof term for the current goal is (add_SNo_Lt3a 0 0 1 (abs_SNo a) SNo_0 SNo_0 SNo_1 HabsS SNoLt_0_1 H0le_abs).
rewrite the current goal using (add_SNo_0L 0 SNo_0) (from right to left) at position 1.
An exact proof term for the current goal is HdenPos0.
We prove the intermediate claim HcLt0S: c < 0.
We prove the intermediate claim HabsR: abs_SNo a ∈ R.
An exact proof term for the current goal is (abs_SNo_in_R a HaR).
We prove the intermediate claim HabsS: SNo (abs_SNo a).
An exact proof term for the current goal is (real_SNo (abs_SNo a) HabsR).
We prove the intermediate claim HdenS: SNo (add_SNo 1 (abs_SNo a)).
An exact proof term for the current goal is (SNo_add_SNo 1 (abs_SNo a) SNo_1 HabsS).
We prove the intermediate claim HphiDef: bounded_transform_phi = graph R (λt0 : set ⇒ div_SNo t0 (add_SNo 1 (abs_SNo t0))).
Use reflexivity.
We prove the intermediate claim HcEq: c = div_SNo a (add_SNo 1 (abs_SNo a)).
rewrite the current goal using HphiDef (from left to right).
rewrite the current goal using (apply_fun_graph R (λt0 : set ⇒ div_SNo t0 (add_SNo 1 (abs_SNo t0))) a HaR) (from left to right).
Use reflexivity.
rewrite the current goal using HcEq (from left to right).
An exact proof term for the current goal is (div_SNo_neg_pos a (add_SNo 1 (abs_SNo a)) HaS HdenS Halt0S HdenApos).
We prove the intermediate claim HcLtS: c < s.
An exact proof term for the current goal is (SNoLtLe_tra c 0 s HcS SNo_0 HsS HcLt0S H0les).
We prove the intermediate claim HcLt: Rlt c s.
An exact proof term for the current goal is (RltI c s HcR HsR HcLtS).
We prove the intermediate claim HrelC: order_rel R c s.
An exact proof term for the current goal is (Rlt_implies_order_rel_R c s HcLt).
We prove the intermediate claim HsRayC: s ∈ open_ray_upper R c.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R c x0) s HsR HrelC).
An exact proof term for the current goal is (binintersectI (open_ray_upper R c) I s HsRayC HsI).
Assume Hn0les: ¬ (0 ≤ s).
We prove the intermediate claim HsLt0S: s < 0.
Apply (SNoLt_trichotomy_or_impred s 0 HsS SNo_0 (s < 0)) to the current goal.
Assume H: s < 0.
An exact proof term for the current goal is H.
Assume Hs0: s = 0.
We prove the intermediate claim H0les: 0 ≤ s.
rewrite the current goal using Hs0 (from left to right).
An exact proof term for the current goal is (SNoLe_ref 0).
An exact proof term for the current goal is (FalseE (Hn0les H0les) (s < 0)).
Assume H0lts: 0 < s.
We prove the intermediate claim H0les: 0 ≤ s.
An exact proof term for the current goal is (SNoLtLe 0 s H0lts).
An exact proof term for the current goal is (FalseE (Hn0les H0les) (s < 0)).
We prove the intermediate claim HsLt0: Rlt s 0.
An exact proof term for the current goal is (RltI s 0 HsR real_0 HsLt0S).
We prove the intermediate claim Hbds: Rlt (minus_SNo 1) s ∧ Rlt s 1.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt (minus_SNo 1) x0 ∧ Rlt x0 1) s HsI).
We prove the intermediate claim Hm1lts: Rlt (minus_SNo 1) s.
An exact proof term for the current goal is (andEL (Rlt (minus_SNo 1) s) (Rlt s 1) Hbds).
We prove the intermediate claim Hm1ltsS: minus_SNo 1 < s.
An exact proof term for the current goal is (RltE_lt (minus_SNo 1) s Hm1lts).
We prove the intermediate claim H0Lt1sS0: add_SNo 1 (minus_SNo 1) < add_SNo 1 s.
An exact proof term for the current goal is (add_SNo_Lt2 1 (minus_SNo 1) s SNo_1 (SNo_minus_SNo 1 SNo_1) HsS Hm1ltsS).
We prove the intermediate claim H0Lt1sS: 0 < add_SNo 1 s.
rewrite the current goal using (add_SNo_minus_SNo_rinv 1 SNo_1) (from right to left) at position 1.
An exact proof term for the current goal is H0Lt1sS0.
We prove the intermediate claim HabsEq: abs_SNo s = minus_SNo s.
An exact proof term for the current goal is (not_nonneg_abs_SNo s Hn0les).
We prove the intermediate claim HdenEq: add_SNo 1 (minus_SNo (abs_SNo s)) = add_SNo 1 s.
rewrite the current goal using HabsEq (from left to right).
rewrite the current goal using (minus_SNo_invol s HsS) (from left to right).
Use reflexivity.
We prove the intermediate claim HpsiDef: bounded_transform_psi = graph R (λs0 : set ⇒ div_SNo s0 (add_SNo 1 (minus_SNo (abs_SNo s0)))).
Use reflexivity.
We prove the intermediate claim HpsiEq0: apply_fun bounded_transform_psi s = div_SNo s (add_SNo 1 (minus_SNo (abs_SNo s))).
rewrite the current goal using HpsiDef (from left to right).
rewrite the current goal using (apply_fun_graph R (λs0 : set ⇒ div_SNo s0 (add_SNo 1 (minus_SNo (abs_SNo s0)))) s HsR) (from left to right).
Use reflexivity.
We prove the intermediate claim HpsiEq: apply_fun bounded_transform_psi s = div_SNo s (add_SNo 1 s).
rewrite the current goal using HpsiEq0 (from left to right).
rewrite the current goal using HdenEq (from left to right).
Use reflexivity.
We prove the intermediate claim HaltAS: a < div_SNo s (add_SNo 1 s).
We prove the intermediate claim HaltS: a < apply_fun bounded_transform_psi s.
An exact proof term for the current goal is (RltE_lt a (apply_fun bounded_transform_psi s) HaltA).
rewrite the current goal using HpsiEq (from right to left) at position 1.
An exact proof term for the current goal is HaltS.
We prove the intermediate claim HdenS: SNo (add_SNo 1 s).
An exact proof term for the current goal is (SNo_add_SNo 1 s SNo_1 HsS).
We prove the intermediate claim HmulLt: mul_SNo a (add_SNo 1 s) < s.
An exact proof term for the current goal is (div_SNo_pos_LtR' s (add_SNo 1 s) a HsS HdenS HaS H0Lt1sS HaltAS).
We prove the intermediate claim Ha1sEq: mul_SNo a (add_SNo 1 s) = add_SNo (mul_SNo a 1) (mul_SNo a s).
An exact proof term for the current goal is (mul_SNo_distrL a 1 s HaS SNo_1 HsS).
We prove the intermediate claim Ha1Eq: mul_SNo a 1 = a.
An exact proof term for the current goal is (mul_SNo_oneR a HaS).
We prove the intermediate claim HmulLt2: add_SNo a (mul_SNo a s) < s.
We prove the intermediate claim Ha1sEq2: mul_SNo a (add_SNo 1 s) = add_SNo a (mul_SNo a s).
rewrite the current goal using Ha1sEq (from left to right).
rewrite the current goal using Ha1Eq (from left to right).
Use reflexivity.
rewrite the current goal using Ha1sEq2 (from right to left) at position 1.
An exact proof term for the current goal is HmulLt.
Set kas to be the term minus_SNo (mul_SNo a s).
We prove the intermediate claim HkasS: SNo kas.
An exact proof term for the current goal is (SNo_minus_SNo (mul_SNo a s) (SNo_mul_SNo a s HaS HsS)).
We prove the intermediate claim HsumLt: add_SNo kas (add_SNo a (mul_SNo a s)) < add_SNo kas s.
An exact proof term for the current goal is (add_SNo_Lt2 kas (add_SNo a (mul_SNo a s)) s HkasS (SNo_add_SNo a (mul_SNo a s) HaS (SNo_mul_SNo a s HaS HsS)) HsS HmulLt2).
We prove the intermediate claim HlhsEq0: add_SNo kas (add_SNo a (mul_SNo a s)) = a.
rewrite the current goal using (add_SNo_assoc kas a (mul_SNo a s) HkasS HaS (SNo_mul_SNo a s HaS HsS)) (from left to right).
rewrite the current goal using (add_SNo_com kas a HkasS HaS) (from left to right) at position 1.
rewrite the current goal using (add_SNo_assoc a kas (mul_SNo a s) HaS HkasS (SNo_mul_SNo a s HaS HsS)) (from right to left) at position 1.
rewrite the current goal using (add_SNo_minus_SNo_linv (mul_SNo a s) (SNo_mul_SNo a s HaS HsS)) (from left to right) at position 1.
rewrite the current goal using (add_SNo_0R a HaS) (from left to right).
Use reflexivity.
We prove the intermediate claim HrhsEq0: add_SNo kas s = add_SNo s (minus_SNo (mul_SNo a s)).
rewrite the current goal using (add_SNo_com kas s HkasS HsS) (from left to right).
Use reflexivity.
We prove the intermediate claim HaLt: a < add_SNo s (minus_SNo (mul_SNo a s)).
rewrite the current goal using HlhsEq0 (from right to left) at position 1.
rewrite the current goal using HrhsEq0 (from right to left) at position 1.
An exact proof term for the current goal is HsumLt.
We prove the intermediate claim Hn0lea: ¬ (0 ≤ a).
Assume H0lea: 0 ≤ a.
We prove the intermediate claim Hcases: 0 < a ∨ 0 = a.
An exact proof term for the current goal is (SNoLeE 0 a SNo_0 HaS H0lea).
Apply Hcases to the current goal.
Assume H0lta: 0 < a.
We prove the intermediate claim H00: 0 < 0.
An exact proof term for the current goal is (SNoLt_tra 0 a 0 SNo_0 HaS SNo_0 H0lta Halt0S).
An exact proof term for the current goal is (FalseE ((SNoLt_irref 0) H00) False).
Assume H0eq: 0 = a.
We prove the intermediate claim Ha0: a = 0.
rewrite the current goal using H0eq (from right to left).
Use reflexivity.
We prove the intermediate claim H00: 0 < 0.
rewrite the current goal using Ha0 (from right to left) at position 1.
An exact proof term for the current goal is Halt0S.
An exact proof term for the current goal is (FalseE ((SNoLt_irref 0) H00) False).
We prove the intermediate claim HabsAeq: abs_SNo a = minus_SNo a.
An exact proof term for the current goal is (not_nonneg_abs_SNo a Hn0lea).
We prove the intermediate claim HphiDef: bounded_transform_phi = graph R (λt0 : set ⇒ div_SNo t0 (add_SNo 1 (abs_SNo t0))).
Use reflexivity.
We prove the intermediate claim HcEq0: c = div_SNo a (add_SNo 1 (abs_SNo a)).
rewrite the current goal using HphiDef (from left to right).
rewrite the current goal using (apply_fun_graph R (λt0 : set ⇒ div_SNo t0 (add_SNo 1 (abs_SNo t0))) a HaR) (from left to right).
Use reflexivity.
We prove the intermediate claim HcEq: c = div_SNo a (add_SNo 1 (minus_SNo a)).
rewrite the current goal using HcEq0 (from left to right).
rewrite the current goal using HabsAeq (from left to right).
Use reflexivity.
We prove the intermediate claim HdenApos: 0 < add_SNo 1 (minus_SNo a).
We prove the intermediate claim HmaS: SNo (minus_SNo a).
An exact proof term for the current goal is (SNo_minus_SNo a HaS).
We prove the intermediate claim H0ltma: 0 < minus_SNo a.
We prove the intermediate claim H0ltma0: minus_SNo 0 < minus_SNo a.
An exact proof term for the current goal is (minus_SNo_Lt_contra a 0 HaS SNo_0 Halt0S).
rewrite the current goal using (minus_SNo_0) (from right to left) at position 1.
An exact proof term for the current goal is H0ltma0.
We prove the intermediate claim H0lema: 0 ≤ minus_SNo a.
An exact proof term for the current goal is (SNoLtLe 0 (minus_SNo a) H0ltma).
We prove the intermediate claim HdenPos0: add_SNo 0 0 < add_SNo 1 (minus_SNo a).
An exact proof term for the current goal is (add_SNo_Lt3a 0 0 1 (minus_SNo a) SNo_0 SNo_0 SNo_1 HmaS SNoLt_0_1 H0lema).
rewrite the current goal using (add_SNo_0L 0 SNo_0) (from right to left) at position 1.
An exact proof term for the current goal is HdenPos0.
We prove the intermediate claim HdenAS: SNo (add_SNo 1 (minus_SNo a)).
An exact proof term for the current goal is (SNo_add_SNo 1 (minus_SNo a) SNo_1 (SNo_minus_SNo a HaS)).
We prove the intermediate claim HmulSA: mul_SNo s (add_SNo 1 (minus_SNo a)) = add_SNo s (minus_SNo (mul_SNo a s)).
rewrite the current goal using (mul_SNo_com s (add_SNo 1 (minus_SNo a)) HsS HdenAS) (from left to right) at position 1.
rewrite the current goal using (mul_SNo_distrR 1 (minus_SNo a) s SNo_1 (SNo_minus_SNo a HaS) HsS) (from left to right).
rewrite the current goal using (mul_SNo_oneL s HsS) (from left to right) at position 1.
rewrite the current goal using (mul_SNo_com (minus_SNo a) s (SNo_minus_SNo a HaS) HsS) (from left to right) at position 1.
rewrite the current goal using (mul_SNo_minus_distrR s a HsS HaS) (from left to right) at position 1.
rewrite the current goal using (mul_SNo_com s a HsS HaS) (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim HaLt2: a < mul_SNo s (add_SNo 1 (minus_SNo a)).
rewrite the current goal using HmulSA (from left to right) at position 1.
An exact proof term for the current goal is HaLt.
We prove the intermediate claim HcLtS: div_SNo a (add_SNo 1 (minus_SNo a)) < s.
An exact proof term for the current goal is (div_SNo_pos_LtL a (add_SNo 1 (minus_SNo a)) s HaS HdenAS HsS HdenApos HaLt2).
We prove the intermediate claim HcLtS': c < s.
rewrite the current goal using HcEq (from left to right).
An exact proof term for the current goal is HcLtS.
We prove the intermediate claim HcLt: Rlt c s.
An exact proof term for the current goal is (RltI c s HcR HsR HcLtS').
We prove the intermediate claim HrelC: order_rel R c s.
An exact proof term for the current goal is (Rlt_implies_order_rel_R c s HcLt).
We prove the intermediate claim HsRayC: s ∈ open_ray_upper R c.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R c x0) s HsR HrelC).
An exact proof term for the current goal is (binintersectI (open_ray_upper R c) I s HsRayC HsI).
Assume Hnlt0: ¬ (Rlt a 0).
We prove the intermediate claim HaNonneg: 0 ≤ a.
Apply (SNoLt_trichotomy_or_impred a 0 HaS SNo_0 (0 ≤ a)) to the current goal.
Assume Halt0S': a < 0.
Apply FalseE to the current goal.
We prove the intermediate claim Halt0': Rlt a 0.
An exact proof term for the current goal is (RltI a 0 HaR real_0 Halt0S').
An exact proof term for the current goal is (Hnlt0 Halt0').
Assume Ha0: a = 0.
rewrite the current goal using Ha0 (from left to right).
An exact proof term for the current goal is (SNoLe_ref 0).
Assume H0lta: 0 < a.
An exact proof term for the current goal is (SNoLtLe 0 a H0lta).
We prove the intermediate claim HpsiS: SNo (apply_fun bounded_transform_psi s).
An exact proof term for the current goal is (real_SNo (apply_fun bounded_transform_psi s) HpsiR).
We prove the intermediate claim HaltAS: a < apply_fun bounded_transform_psi s.
An exact proof term for the current goal is (RltE_lt a (apply_fun bounded_transform_psi s) HaltA).
We prove the intermediate claim H0ltPsi: 0 < apply_fun bounded_transform_psi s.
An exact proof term for the current goal is (SNoLeLt_tra 0 a (apply_fun bounded_transform_psi s) SNo_0 HaS HpsiS HaNonneg HaltAS).
We prove the intermediate claim HabsR: abs_SNo s ∈ R.
An exact proof term for the current goal is (abs_SNo_in_R s HsR).
We prove the intermediate claim HabsS: SNo (abs_SNo s).
An exact proof term for the current goal is (real_SNo (abs_SNo s) HabsR).
We prove the intermediate claim Hbds: Rlt (minus_SNo 1) s ∧ Rlt s 1.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt (minus_SNo 1) x0 ∧ Rlt x0 1) s HsI).
We prove the intermediate claim Hslt1: Rlt s 1.
An exact proof term for the current goal is (andER (Rlt (minus_SNo 1) s) (Rlt s 1) Hbds).
We prove the intermediate claim Hslt1S: s < 1.
An exact proof term for the current goal is (RltE_lt s 1 Hslt1).
We prove the intermediate claim HabLt1: abs_SNo s < 1.
Apply (xm (0 ≤ s)) to the current goal.
Assume H0les: 0 ≤ s.
rewrite the current goal using (nonneg_abs_SNo s H0les) (from left to right).
An exact proof term for the current goal is Hslt1S.
Assume Hn0les: ¬ (0 ≤ s).
We prove the intermediate claim Hslt0: s < 0.
Apply (SNoLt_trichotomy_or_impred s 0 HsS SNo_0 (s < 0)) to the current goal.
Assume H: s < 0.
An exact proof term for the current goal is H.
Assume Hs0: s = 0.
We prove the intermediate claim H0les: 0 ≤ s.
rewrite the current goal using Hs0 (from left to right).
An exact proof term for the current goal is (SNoLe_ref 0).
An exact proof term for the current goal is (FalseE (Hn0les H0les) (s < 0)).
Assume H0lts: 0 < s.
We prove the intermediate claim H0les: 0 ≤ s.
An exact proof term for the current goal is (SNoLtLe 0 s H0lts).
An exact proof term for the current goal is (FalseE (Hn0les H0les) (s < 0)).
rewrite the current goal using (not_nonneg_abs_SNo s Hn0les) (from left to right).
We prove the intermediate claim Hm1lts: Rlt (minus_SNo 1) s.
An exact proof term for the current goal is (andEL (Rlt (minus_SNo 1) s) (Rlt s 1) Hbds).
We prove the intermediate claim Hm1ltsS: minus_SNo 1 < s.
An exact proof term for the current goal is (RltE_lt (minus_SNo 1) s Hm1lts).
We prove the intermediate claim HmsLt1: minus_SNo s < 1.
We prove the intermediate claim HmsLt1': minus_SNo s < minus_SNo (minus_SNo 1).
An exact proof term for the current goal is (minus_SNo_Lt_contra (minus_SNo 1) s (SNo_minus_SNo 1 SNo_1) HsS Hm1ltsS).
rewrite the current goal using (minus_SNo_invol 1 SNo_1) (from right to left) at position 1.
An exact proof term for the current goal is HmsLt1'.
An exact proof term for the current goal is HmsLt1.
Set den to be the term add_SNo 1 (minus_SNo (abs_SNo s)).
We prove the intermediate claim HdenS: SNo den.
An exact proof term for the current goal is (SNo_add_SNo 1 (minus_SNo (abs_SNo s)) SNo_1 (SNo_minus_SNo (abs_SNo s) HabsS)).
We prove the intermediate claim HdenPos0: add_SNo 1 (minus_SNo 1) < den.
We prove the intermediate claim Hneg1LtNegAbs: minus_SNo 1 < minus_SNo (abs_SNo s).
An exact proof term for the current goal is (minus_SNo_Lt_contra (abs_SNo s) 1 HabsS SNo_1 HabLt1).
An exact proof term for the current goal is (add_SNo_Lt2 1 (minus_SNo 1) (minus_SNo (abs_SNo s)) SNo_1 (SNo_minus_SNo 1 SNo_1) (SNo_minus_SNo (abs_SNo s) HabsS) Hneg1LtNegAbs).
We prove the intermediate claim HdenPos: 0 < den.
rewrite the current goal using (add_SNo_minus_SNo_rinv 1 SNo_1) (from right to left) at position 1.
An exact proof term for the current goal is HdenPos0.
We prove the intermediate claim HpsiEq0: apply_fun bounded_transform_psi s = div_SNo s den.
We prove the intermediate claim HpsiDef: bounded_transform_psi = graph R (λs0 : set ⇒ div_SNo s0 (add_SNo 1 (minus_SNo (abs_SNo s0)))).
Use reflexivity.
rewrite the current goal using HpsiDef (from left to right).
rewrite the current goal using (apply_fun_graph R (λs0 : set ⇒ div_SNo s0 (add_SNo 1 (minus_SNo (abs_SNo s0)))) s HsR) (from left to right).
Use reflexivity.
We prove the intermediate claim H0ltDiv: 0 < div_SNo s den.
rewrite the current goal using HpsiEq0 (from right to left) at position 1.
An exact proof term for the current goal is H0ltPsi.
We prove the intermediate claim H0LtS_raw: mul_SNo 0 den < s.
An exact proof term for the current goal is (div_SNo_pos_LtR' s den 0 HsS HdenS SNo_0 HdenPos H0ltDiv).
We prove the intermediate claim H0LtS: 0 < s.
rewrite the current goal using (mul_SNo_zeroL den HdenS) (from right to left) at position 1.
An exact proof term for the current goal is H0LtS_raw.
We prove the intermediate claim H0les: 0 ≤ s.
An exact proof term for the current goal is (SNoLtLe 0 s H0LtS).
We prove the intermediate claim HabsEq: abs_SNo s = s.
An exact proof term for the current goal is (nonneg_abs_SNo s H0les).
We prove the intermediate claim HdenEq: den = add_SNo 1 (minus_SNo s).
rewrite the current goal using HabsEq (from left to right).
Use reflexivity.
We prove the intermediate claim HpsiEq: apply_fun bounded_transform_psi s = div_SNo s (add_SNo 1 (minus_SNo s)).
rewrite the current goal using HpsiEq0 (from left to right).
rewrite the current goal using HdenEq (from left to right).
Use reflexivity.
We prove the intermediate claim HaltAS2: a < div_SNo s (add_SNo 1 (minus_SNo s)).
rewrite the current goal using HpsiEq (from right to left) at position 1.
An exact proof term for the current goal is HaltAS.
We prove the intermediate claim Hden2S: SNo (add_SNo 1 (minus_SNo s)).
An exact proof term for the current goal is (SNo_add_SNo 1 (minus_SNo s) SNo_1 (SNo_minus_SNo s HsS)).
We prove the intermediate claim Hden2Pos0: add_SNo (minus_SNo s) s < add_SNo (minus_SNo s) 1.
An exact proof term for the current goal is (add_SNo_Lt2 (minus_SNo s) s 1 (SNo_minus_SNo s HsS) HsS SNo_1 Hslt1S).
We prove the intermediate claim Hden2Pos: 0 < add_SNo 1 (minus_SNo s).
We prove the intermediate claim Htmp: 0 < add_SNo (minus_SNo s) 1.
rewrite the current goal using (add_SNo_minus_SNo_linv s HsS) (from right to left) at position 1.
An exact proof term for the current goal is Hden2Pos0.
rewrite the current goal using (add_SNo_com (minus_SNo s) 1 (SNo_minus_SNo s HsS) SNo_1) (from right to left) at position 1.
An exact proof term for the current goal is Htmp.
We prove the intermediate claim HmulLt: mul_SNo a (add_SNo 1 (minus_SNo s)) < s.
An exact proof term for the current goal is (div_SNo_pos_LtR' s (add_SNo 1 (minus_SNo s)) a HsS Hden2S HaS Hden2Pos HaltAS2).
We prove the intermediate claim HmulEq: mul_SNo a (add_SNo 1 (minus_SNo s)) = add_SNo a (minus_SNo (mul_SNo a s)).
rewrite the current goal using (mul_SNo_distrL a 1 (minus_SNo s) HaS SNo_1 (SNo_minus_SNo s HsS)) (from left to right).
rewrite the current goal using (mul_SNo_oneR a HaS) (from left to right) at position 1.
rewrite the current goal using (mul_SNo_minus_distrR a s HaS HsS) (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim HmulLt2: add_SNo a (minus_SNo (mul_SNo a s)) < s.
rewrite the current goal using HmulEq (from right to left) at position 1.
An exact proof term for the current goal is HmulLt.
Set kas to be the term mul_SNo a s.
We prove the intermediate claim HkasS: SNo kas.
An exact proof term for the current goal is (SNo_mul_SNo a s HaS HsS).
We prove the intermediate claim HsumLt: add_SNo kas (add_SNo a (minus_SNo kas)) < add_SNo kas s.
An exact proof term for the current goal is (add_SNo_Lt2 kas (add_SNo a (minus_SNo kas)) s HkasS (SNo_add_SNo a (minus_SNo kas) HaS (SNo_minus_SNo kas HkasS)) HsS HmulLt2).
We prove the intermediate claim HlhsEq0: add_SNo kas (add_SNo a (minus_SNo kas)) = a.
rewrite the current goal using (add_SNo_assoc kas a (minus_SNo kas) HkasS HaS (SNo_minus_SNo kas HkasS)) (from left to right).
rewrite the current goal using (add_SNo_com kas a HkasS HaS) (from left to right) at position 1.
rewrite the current goal using (add_SNo_assoc a kas (minus_SNo kas) HaS HkasS (SNo_minus_SNo kas HkasS)) (from right to left) at position 1.
rewrite the current goal using (add_SNo_minus_SNo_rinv kas HkasS) (from left to right) at position 1.
rewrite the current goal using (add_SNo_0R a HaS) (from left to right).
Use reflexivity.
We prove the intermediate claim HrhsEq0: add_SNo kas s = add_SNo s kas.
rewrite the current goal using (add_SNo_com kas s HkasS HsS) (from left to right).
Use reflexivity.
We prove the intermediate claim HaLt: a < add_SNo s (mul_SNo a s).
rewrite the current goal using HlhsEq0 (from right to left) at position 1.
rewrite the current goal using HrhsEq0 (from right to left) at position 1.
An exact proof term for the current goal is HsumLt.
We prove the intermediate claim HdenApos: 0 < add_SNo 1 a.
We prove the intermediate claim H0leA: 0 ≤ a.
An exact proof term for the current goal is HaNonneg.
We prove the intermediate claim HdenPos0: add_SNo 0 0 < add_SNo 1 a.
An exact proof term for the current goal is (add_SNo_Lt3a 0 0 1 a SNo_0 SNo_0 SNo_1 HaS SNoLt_0_1 H0leA).
rewrite the current goal using (add_SNo_0L 0 SNo_0) (from right to left) at position 1.
An exact proof term for the current goal is HdenPos0.
We prove the intermediate claim HdenAS: SNo (add_SNo 1 a).
An exact proof term for the current goal is (SNo_add_SNo 1 a SNo_1 HaS).
We prove the intermediate claim HcEq0: c = div_SNo a (add_SNo 1 (abs_SNo a)).
We prove the intermediate claim HphiDef: bounded_transform_phi = graph R (λt0 : set ⇒ div_SNo t0 (add_SNo 1 (abs_SNo t0))).
Use reflexivity.
rewrite the current goal using HphiDef (from left to right).
rewrite the current goal using (apply_fun_graph R (λt0 : set ⇒ div_SNo t0 (add_SNo 1 (abs_SNo t0))) a HaR) (from left to right).
Use reflexivity.
We prove the intermediate claim HcEq: c = div_SNo a (add_SNo 1 a).
rewrite the current goal using HcEq0 (from left to right).
rewrite the current goal using (nonneg_abs_SNo a HaNonneg) (from left to right).
Use reflexivity.
We prove the intermediate claim HcLtS: div_SNo a (add_SNo 1 a) < s.
We prove the intermediate claim HmulSA: mul_SNo s (add_SNo 1 a) = add_SNo s (mul_SNo a s).
rewrite the current goal using (mul_SNo_distrL s 1 a HsS SNo_1 HaS) (from left to right).
rewrite the current goal using (mul_SNo_oneR s HsS) (from left to right) at position 1.
rewrite the current goal using (mul_SNo_com s a HsS HaS) (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim HaLt2: a < mul_SNo s (add_SNo 1 a).
rewrite the current goal using HmulSA (from left to right) at position 1.
An exact proof term for the current goal is HaLt.
An exact proof term for the current goal is (div_SNo_pos_LtL a (add_SNo 1 a) s HaS HdenAS HsS HdenApos HaLt2).
We prove the intermediate claim HcLtS': c < s.
rewrite the current goal using HcEq (from left to right).
An exact proof term for the current goal is HcLtS.
We prove the intermediate claim HcLt: Rlt c s.
An exact proof term for the current goal is (RltI c s HcR HsR HcLtS').
We prove the intermediate claim HrelC: order_rel R c s.
An exact proof term for the current goal is (Rlt_implies_order_rel_R c s HcLt).
We prove the intermediate claim HsRayC: s ∈ open_ray_upper R c.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R c x0) s HsR HrelC).
An exact proof term for the current goal is (binintersectI (open_ray_upper R c) I s HsRayC HsI).
Let s be given.
Assume HsInt: s ∈ (open_ray_upper R c) ∩ I.
We will prove s ∈ U.
We prove the intermediate claim HsRayC: s ∈ open_ray_upper R c.
An exact proof term for the current goal is (binintersectE1 (open_ray_upper R c) I s HsInt).
We prove the intermediate claim HsI: s ∈ I.
An exact proof term for the current goal is (binintersectE2 (open_ray_upper R c) I s HsInt).
rewrite the current goal using HUdef (from left to right).
rewrite the current goal using Hpredef (from left to right).
Apply (SepI I (λx0 : set ⇒ apply_fun bounded_transform_psi x0 ∈ open_ray_upper R a) s HsI) to the current goal.
We prove the intermediate claim HsR: s ∈ R.
An exact proof term for the current goal is (HI_sub_R s HsI).
We prove the intermediate claim HpsiR: apply_fun bounded_transform_psi s ∈ R.
We prove the intermediate claim HabsR: abs_SNo s ∈ R.
An exact proof term for the current goal is (abs_SNo_in_R s HsR).
We prove the intermediate claim HminR: minus_SNo (abs_SNo s) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (abs_SNo s) HabsR).
We prove the intermediate claim HdenR: add_SNo 1 (minus_SNo (abs_SNo s)) ∈ R.
An exact proof term for the current goal is (real_add_SNo 1 real_1 (minus_SNo (abs_SNo s)) HminR).
We prove the intermediate claim HpsiDef: bounded_transform_psi = graph R (λs0 : set ⇒ div_SNo s0 (add_SNo 1 (minus_SNo (abs_SNo s0)))).
Use reflexivity.
rewrite the current goal using HpsiDef (from left to right).
rewrite the current goal using (apply_fun_graph R (λs0 : set ⇒ div_SNo s0 (add_SNo 1 (minus_SNo (abs_SNo s0)))) s HsR) (from left to right).
An exact proof term for the current goal is (real_div_SNo s HsR (add_SNo 1 (minus_SNo (abs_SNo s))) HdenR).
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 HsS: SNo s.
An exact proof term for the current goal is (real_SNo s HsR).
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 HrelC: order_rel R c s.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R c x0) s HsRayC).
We prove the intermediate claim HcLt: Rlt c s.
An exact proof term for the current goal is (order_rel_R_implies_Rlt c s HrelC).
We prove the intermediate claim HcLtS: c < s.
An exact proof term for the current goal is (RltE_lt c s HcLt).
Apply (xm (Rlt a 0)) to the current goal.
Assume Halt0: Rlt a 0.
We prove the intermediate claim Halt0S: a < 0.
An exact proof term for the current goal is (RltE_lt a 0 Halt0).
Apply (xm (0 ≤ s)) to the current goal.
Assume H0les: 0 ≤ s.
Set den to be the term add_SNo 1 (minus_SNo (abs_SNo s)).
We prove the intermediate claim HabsR: abs_SNo s ∈ R.
An exact proof term for the current goal is (abs_SNo_in_R s HsR).
We prove the intermediate claim HabsS: SNo (abs_SNo s).
An exact proof term for the current goal is (real_SNo (abs_SNo s) HabsR).
We prove the intermediate claim HdenS: SNo den.
An exact proof term for the current goal is (SNo_add_SNo 1 (minus_SNo (abs_SNo s)) SNo_1 (SNo_minus_SNo (abs_SNo s) HabsS)).
We prove the intermediate claim Hbds: Rlt (minus_SNo 1) s ∧ Rlt s 1.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt (minus_SNo 1) x0 ∧ Rlt x0 1) s HsI).
We prove the intermediate claim Hslt1: Rlt s 1.
An exact proof term for the current goal is (andER (Rlt (minus_SNo 1) s) (Rlt s 1) Hbds).
We prove the intermediate claim Hslt1S: s < 1.
An exact proof term for the current goal is (RltE_lt s 1 Hslt1).
We prove the intermediate claim HabLt1: abs_SNo s < 1.
rewrite the current goal using (nonneg_abs_SNo s H0les) (from left to right).
An exact proof term for the current goal is Hslt1S.
We prove the intermediate claim Hneg1LtNegAbs: minus_SNo 1 < minus_SNo (abs_SNo s).
An exact proof term for the current goal is (minus_SNo_Lt_contra (abs_SNo s) 1 HabsS SNo_1 HabLt1).
We prove the intermediate claim HdenPos0: add_SNo 1 (minus_SNo 1) < den.
An exact proof term for the current goal is (add_SNo_Lt2 1 (minus_SNo 1) (minus_SNo (abs_SNo s)) SNo_1 (SNo_minus_SNo 1 SNo_1) (SNo_minus_SNo (abs_SNo s) HabsS) Hneg1LtNegAbs).
We prove the intermediate claim HdenPos: 0 < den.
rewrite the current goal using (add_SNo_minus_SNo_rinv 1 SNo_1) (from right to left) at position 1.
An exact proof term for the current goal is HdenPos0.
We prove the intermediate claim HpsiEq: apply_fun bounded_transform_psi s = div_SNo s den.
We prove the intermediate claim HpsiDef: bounded_transform_psi = graph R (λs0 : set ⇒ div_SNo s0 (add_SNo 1 (minus_SNo (abs_SNo s0)))).
Use reflexivity.
rewrite the current goal using HpsiDef (from left to right).
rewrite the current goal using (apply_fun_graph R (λs0 : set ⇒ div_SNo s0 (add_SNo 1 (minus_SNo (abs_SNo s0)))) s HsR) (from left to right).
Use reflexivity.
We prove the intermediate claim HpsiS: SNo (apply_fun bounded_transform_psi s).
An exact proof term for the current goal is (real_SNo (apply_fun bounded_transform_psi s) HpsiR).
We prove the intermediate claim H0lePsi: 0 ≤ apply_fun bounded_transform_psi s.
rewrite the current goal using HpsiEq (from left to right).
An exact proof term for the current goal is (div_SNo_nonneg_pos_nonneg s den HsS HdenS H0les HdenPos).
We prove the intermediate claim HaltPsiS: a < apply_fun bounded_transform_psi s.
An exact proof term for the current goal is (SNoLtLe_tra a 0 (apply_fun bounded_transform_psi s) HaS SNo_0 HpsiS Halt0S H0lePsi).
We prove the intermediate claim HaltPsi: Rlt a (apply_fun bounded_transform_psi s).
An exact proof term for the current goal is (RltI a (apply_fun bounded_transform_psi s) HaR HpsiR HaltPsiS).
We prove the intermediate claim HrelA: order_rel R a (apply_fun bounded_transform_psi s).
An exact proof term for the current goal is (Rlt_implies_order_rel_R a (apply_fun bounded_transform_psi s) HaltPsi).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R a x0) (apply_fun bounded_transform_psi s) HpsiR HrelA).
Assume Hn0les: ¬ (0 ≤ s).
Set denA to be the term add_SNo 1 (minus_SNo a).
We prove the intermediate claim Hn0lea: ¬ (0 ≤ a).
Assume H0lea: 0 ≤ a.
We prove the intermediate claim Hcases: 0 < a ∨ 0 = a.
An exact proof term for the current goal is (SNoLeE 0 a SNo_0 HaS H0lea).
Apply Hcases to the current goal.
Assume H0lta: 0 < a.
We prove the intermediate claim H00: 0 < 0.
An exact proof term for the current goal is (SNoLt_tra 0 a 0 SNo_0 HaS SNo_0 H0lta Halt0S).
An exact proof term for the current goal is (FalseE ((SNoLt_irref 0) H00) False).
Assume H0eq: 0 = a.
We prove the intermediate claim Ha0: a = 0.
rewrite the current goal using H0eq (from right to left).
Use reflexivity.
We prove the intermediate claim H00: 0 < 0.
rewrite the current goal using Ha0 (from right to left) at position 1.
An exact proof term for the current goal is Halt0S.
An exact proof term for the current goal is (FalseE ((SNoLt_irref 0) H00) False).
We prove the intermediate claim HabsAeq: abs_SNo a = minus_SNo a.
An exact proof term for the current goal is (not_nonneg_abs_SNo a Hn0lea).
We prove the intermediate claim HphiDef: bounded_transform_phi = graph R (λt0 : set ⇒ div_SNo t0 (add_SNo 1 (abs_SNo t0))).
Use reflexivity.
We prove the intermediate claim HcEq0: c = div_SNo a (add_SNo 1 (abs_SNo a)).
rewrite the current goal using HphiDef (from left to right).
rewrite the current goal using (apply_fun_graph R (λt0 : set ⇒ div_SNo t0 (add_SNo 1 (abs_SNo t0))) a HaR) (from left to right).
Use reflexivity.
We prove the intermediate claim HcEq: c = div_SNo a denA.
rewrite the current goal using HcEq0 (from left to right).
rewrite the current goal using HabsAeq (from left to right).
Use reflexivity.
We prove the intermediate claim HdenAS: SNo denA.
An exact proof term for the current goal is (SNo_add_SNo 1 (minus_SNo a) SNo_1 (SNo_minus_SNo a HaS)).
We prove the intermediate claim HmaS: SNo (minus_SNo a).
An exact proof term for the current goal is (SNo_minus_SNo a HaS).
We prove the intermediate claim H0ltma: 0 < minus_SNo a.
We prove the intermediate claim H0ltma0: minus_SNo 0 < minus_SNo a.
An exact proof term for the current goal is (minus_SNo_Lt_contra a 0 HaS SNo_0 Halt0S).
rewrite the current goal using (minus_SNo_0) (from right to left) at position 1.
An exact proof term for the current goal is H0ltma0.
We prove the intermediate claim H0lema: 0 ≤ minus_SNo a.
An exact proof term for the current goal is (SNoLtLe 0 (minus_SNo a) H0ltma).
We prove the intermediate claim HdenApos0: add_SNo 0 0 < denA.
An exact proof term for the current goal is (add_SNo_Lt3a 0 0 1 (minus_SNo a) SNo_0 SNo_0 SNo_1 HmaS SNoLt_0_1 H0lema).
We prove the intermediate claim HdenApos: 0 < denA.
rewrite the current goal using (add_SNo_0L 0 SNo_0) (from right to left) at position 1.
An exact proof term for the current goal is HdenApos0.
We prove the intermediate claim HcLtS2: div_SNo a denA < s.
rewrite the current goal using HcEq (from right to left) at position 1.
An exact proof term for the current goal is HcLtS.
We prove the intermediate claim HaLt2: a < mul_SNo s denA.
An exact proof term for the current goal is (div_SNo_pos_LtL' a denA s HaS HdenAS HsS HdenApos HcLtS2).
Set denS to be the term add_SNo 1 s.
We prove the intermediate claim HdenSS: SNo denS.
An exact proof term for the current goal is (SNo_add_SNo 1 s SNo_1 HsS).
We prove the intermediate claim HpsiEq0: apply_fun bounded_transform_psi s = div_SNo s (add_SNo 1 (minus_SNo (abs_SNo s))).
We prove the intermediate claim HpsiDef: bounded_transform_psi = graph R (λs0 : set ⇒ div_SNo s0 (add_SNo 1 (minus_SNo (abs_SNo s0)))).
Use reflexivity.
rewrite the current goal using HpsiDef (from left to right).
rewrite the current goal using (apply_fun_graph R (λs0 : set ⇒ div_SNo s0 (add_SNo 1 (minus_SNo (abs_SNo s0)))) s HsR) (from left to right).
Use reflexivity.
We prove the intermediate claim HabsEq: abs_SNo s = minus_SNo s.
An exact proof term for the current goal is (not_nonneg_abs_SNo s Hn0les).
We prove the intermediate claim HdenEq: add_SNo 1 (minus_SNo (abs_SNo s)) = denS.
rewrite the current goal using HabsEq (from left to right).
rewrite the current goal using (minus_SNo_invol s HsS) (from left to right).
Use reflexivity.
We prove the intermediate claim HpsiEq: apply_fun bounded_transform_psi s = div_SNo s denS.
rewrite the current goal using HpsiEq0 (from left to right).
rewrite the current goal using HdenEq (from left to right).
Use reflexivity.
Set asb to be the term mul_SNo a s.
We prove the intermediate claim HasbS: SNo asb.
An exact proof term for the current goal is (SNo_mul_SNo a s HaS HsS).
We prove the intermediate claim HmulSA: mul_SNo s denA = add_SNo s (minus_SNo asb).
rewrite the current goal using (mul_SNo_distrL s 1 (minus_SNo a) HsS SNo_1 (SNo_minus_SNo a HaS)) (from left to right).
rewrite the current goal using (mul_SNo_oneR s HsS) (from left to right) at position 1.
rewrite the current goal using (mul_SNo_minus_distrR s a HsS HaS) (from left to right) at position 1.
rewrite the current goal using (mul_SNo_com s a HsS HaS) (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim HaLt3: a < add_SNo s (minus_SNo asb).
rewrite the current goal using HmulSA (from right to left) at position 1.
An exact proof term for the current goal is HaLt2.
We prove the intermediate claim Hshift: add_SNo asb a < add_SNo asb (add_SNo s (minus_SNo asb)).
An exact proof term for the current goal is (add_SNo_Lt2 asb a (add_SNo s (minus_SNo asb)) HasbS HaS (SNo_add_SNo s (minus_SNo asb) HsS (SNo_minus_SNo asb HasbS)) HaLt3).
We prove the intermediate claim HlhsEq: add_SNo asb a = add_SNo a asb.
An exact proof term for the current goal is (add_SNo_com asb a HasbS HaS).
We prove the intermediate claim HrhsEq0: add_SNo asb (add_SNo s (minus_SNo asb)) = add_SNo (add_SNo asb s) (minus_SNo asb).
An exact proof term for the current goal is (add_SNo_assoc asb s (minus_SNo asb) HasbS HsS (SNo_minus_SNo asb HasbS)).
We prove the intermediate claim HrhsEq1: add_SNo (add_SNo asb s) (minus_SNo asb) = add_SNo (add_SNo s asb) (minus_SNo asb).
rewrite the current goal using (add_SNo_com asb s HasbS HsS) (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim HrhsEq2: add_SNo (add_SNo s asb) (minus_SNo asb) = add_SNo s (add_SNo asb (minus_SNo asb)).
rewrite the current goal using (add_SNo_assoc s asb (minus_SNo asb) HsS HasbS (SNo_minus_SNo asb HasbS)) (from right to left).
Use reflexivity.
We prove the intermediate claim HrhsEq3: add_SNo asb (minus_SNo asb) = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_rinv asb HasbS).
We prove the intermediate claim HrhsEq: add_SNo asb (add_SNo s (minus_SNo asb)) = s.
rewrite the current goal using HrhsEq0 (from left to right).
rewrite the current goal using HrhsEq1 (from left to right).
rewrite the current goal using HrhsEq2 (from left to right).
rewrite the current goal using HrhsEq3 (from left to right).
rewrite the current goal using (add_SNo_0R s HsS) (from left to right).
Use reflexivity.
We prove the intermediate claim HmulLt: mul_SNo a denS < s.
We prove the intermediate claim HmulDen: mul_SNo a denS = add_SNo a asb.
rewrite the current goal using (mul_SNo_distrL a 1 s HaS SNo_1 HsS) (from left to right).
rewrite the current goal using (mul_SNo_oneR a HaS) (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using HmulDen (from left to right).
rewrite the current goal using HlhsEq (from right to left) at position 1.
rewrite the current goal using HrhsEq (from right to left) at position 2.
An exact proof term for the current goal is Hshift.
We prove the intermediate claim HdenSpos0: add_SNo 1 (minus_SNo 1) < denS.
We prove the intermediate claim Hbds: Rlt (minus_SNo 1) s ∧ Rlt s 1.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt (minus_SNo 1) x0 ∧ Rlt x0 1) s HsI).
We prove the intermediate claim Hm1lts: Rlt (minus_SNo 1) s.
An exact proof term for the current goal is (andEL (Rlt (minus_SNo 1) s) (Rlt s 1) Hbds).
We prove the intermediate claim Hm1ltsS: minus_SNo 1 < s.
An exact proof term for the current goal is (RltE_lt (minus_SNo 1) s Hm1lts).
An exact proof term for the current goal is (add_SNo_Lt2 1 (minus_SNo 1) s SNo_1 (SNo_minus_SNo 1 SNo_1) HsS Hm1ltsS).
We prove the intermediate claim HdenSpos: 0 < denS.
rewrite the current goal using (add_SNo_minus_SNo_rinv 1 SNo_1) (from right to left) at position 1.
An exact proof term for the current goal is HdenSpos0.
We prove the intermediate claim HaltPsiS: a < div_SNo s denS.
An exact proof term for the current goal is (div_SNo_pos_LtR s denS a HsS HdenSS HaS HdenSpos HmulLt).
We prove the intermediate claim HaltPsi: Rlt a (apply_fun bounded_transform_psi s).
We prove the intermediate claim HdenSR: denS ∈ R.
An exact proof term for the current goal is (real_add_SNo 1 real_1 s HsR).
rewrite the current goal using HpsiEq (from left to right).
An exact proof term for the current goal is (RltI a (div_SNo s denS) HaR (real_div_SNo s HsR denS HdenSR) HaltPsiS).
We prove the intermediate claim HrelA: order_rel R a (apply_fun bounded_transform_psi s).
An exact proof term for the current goal is (Rlt_implies_order_rel_R a (apply_fun bounded_transform_psi s) HaltPsi).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R a x0) (apply_fun bounded_transform_psi s) HpsiR HrelA).
Assume Hnlt0a: ¬ (Rlt a 0).
We prove the intermediate claim HaNonneg: 0 ≤ a.
Apply (SNoLt_trichotomy_or_impred a 0 HaS SNo_0 (0 ≤ a)) to the current goal.
Assume Halt0S': a < 0.
Apply FalseE to the current goal.
We prove the intermediate claim Halt0': Rlt a 0.
An exact proof term for the current goal is (RltI a 0 HaR real_0 Halt0S').
An exact proof term for the current goal is (Hnlt0a Halt0').
Assume Ha0: a = 0.
rewrite the current goal using Ha0 (from left to right).
An exact proof term for the current goal is (SNoLe_ref 0).
Assume H0lta: 0 < a.
An exact proof term for the current goal is (SNoLtLe 0 a H0lta).
Set denA to be the term add_SNo 1 a.
We prove the intermediate claim HdenAS: SNo denA.
An exact proof term for the current goal is (SNo_add_SNo 1 a SNo_1 HaS).
We prove the intermediate claim HdenApos0: add_SNo 0 0 < denA.
An exact proof term for the current goal is (add_SNo_Lt3a 0 0 1 a SNo_0 SNo_0 SNo_1 HaS SNoLt_0_1 HaNonneg).
We prove the intermediate claim HdenApos: 0 < denA.
rewrite the current goal using (add_SNo_0L 0 SNo_0) (from right to left) at position 1.
An exact proof term for the current goal is HdenApos0.
We prove the intermediate claim HphiDef: bounded_transform_phi = graph R (λt0 : set ⇒ div_SNo t0 (add_SNo 1 (abs_SNo t0))).
Use reflexivity.
We prove the intermediate claim HcEq0: c = div_SNo a (add_SNo 1 (abs_SNo a)).
rewrite the current goal using HphiDef (from left to right).
rewrite the current goal using (apply_fun_graph R (λt0 : set ⇒ div_SNo t0 (add_SNo 1 (abs_SNo t0))) a HaR) (from left to right).
Use reflexivity.
We prove the intermediate claim HcEq: c = div_SNo a denA.
rewrite the current goal using HcEq0 (from left to right).
rewrite the current goal using (nonneg_abs_SNo a HaNonneg) (from left to right).
Use reflexivity.
We prove the intermediate claim HcLtS2: div_SNo a denA < s.
rewrite the current goal using HcEq (from right to left) at position 1.
An exact proof term for the current goal is HcLtS.
We prove the intermediate claim HaLt2: a < mul_SNo s denA.
An exact proof term for the current goal is (div_SNo_pos_LtL' a denA s HaS HdenAS HsS HdenApos HcLtS2).
We prove the intermediate claim HcNonneg: 0 ≤ c.
rewrite the current goal using HcEq (from left to right).
An exact proof term for the current goal is (div_SNo_nonneg_pos_nonneg a denA HaS HdenAS HaNonneg HdenApos).
We prove the intermediate claim H0ltS: 0 < s.
An exact proof term for the current goal is (SNoLeLt_tra 0 c s SNo_0 HcS HsS HcNonneg HcLtS).
We prove the intermediate claim H0les: 0 ≤ s.
An exact proof term for the current goal is (SNoLtLe 0 s H0ltS).
We prove the intermediate claim HabsEq: abs_SNo s = s.
An exact proof term for the current goal is (nonneg_abs_SNo s H0les).
Set denS to be the term add_SNo 1 (minus_SNo s).
We prove the intermediate claim HdenSS: SNo denS.
An exact proof term for the current goal is (SNo_add_SNo 1 (minus_SNo s) SNo_1 (SNo_minus_SNo s HsS)).
We prove the intermediate claim Hbds: Rlt (minus_SNo 1) s ∧ Rlt s 1.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt (minus_SNo 1) x0 ∧ Rlt x0 1) s HsI).
We prove the intermediate claim Hslt1: Rlt s 1.
An exact proof term for the current goal is (andER (Rlt (minus_SNo 1) s) (Rlt s 1) Hbds).
We prove the intermediate claim Hslt1S: s < 1.
An exact proof term for the current goal is (RltE_lt s 1 Hslt1).
We prove the intermediate claim HdenSpos0: add_SNo (minus_SNo s) s < add_SNo (minus_SNo s) 1.
An exact proof term for the current goal is (add_SNo_Lt2 (minus_SNo s) s 1 (SNo_minus_SNo s HsS) HsS SNo_1 Hslt1S).
We prove the intermediate claim HdenSpos: 0 < denS.
We prove the intermediate claim Htmp: 0 < add_SNo (minus_SNo s) 1.
rewrite the current goal using (add_SNo_minus_SNo_linv s HsS) (from right to left) at position 1.
An exact proof term for the current goal is HdenSpos0.
rewrite the current goal using (add_SNo_com (minus_SNo s) 1 (SNo_minus_SNo s HsS) SNo_1) (from right to left) at position 1.
An exact proof term for the current goal is Htmp.
We prove the intermediate claim HpsiEq0: apply_fun bounded_transform_psi s = div_SNo s (add_SNo 1 (minus_SNo (abs_SNo s))).
We prove the intermediate claim HpsiDef: bounded_transform_psi = graph R (λs0 : set ⇒ div_SNo s0 (add_SNo 1 (minus_SNo (abs_SNo s0)))).
Use reflexivity.
rewrite the current goal using HpsiDef (from left to right).
rewrite the current goal using (apply_fun_graph R (λs0 : set ⇒ div_SNo s0 (add_SNo 1 (minus_SNo (abs_SNo s0)))) s HsR) (from left to right).
Use reflexivity.
We prove the intermediate claim HpsiEq: apply_fun bounded_transform_psi s = div_SNo s denS.
rewrite the current goal using HpsiEq0 (from left to right).
rewrite the current goal using HabsEq (from left to right).
Use reflexivity.
Set asb to be the term mul_SNo a s.
We prove the intermediate claim HasbS: SNo asb.
An exact proof term for the current goal is (SNo_mul_SNo a s HaS HsS).
We prove the intermediate claim HmulSA: mul_SNo s denA = add_SNo s asb.
rewrite the current goal using (mul_SNo_distrL s 1 a HsS SNo_1 HaS) (from left to right).
rewrite the current goal using (mul_SNo_oneR s HsS) (from left to right) at position 1.
rewrite the current goal using (mul_SNo_com s a HsS HaS) (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim HaLt3: a < add_SNo s asb.
rewrite the current goal using HmulSA (from right to left) at position 1.
An exact proof term for the current goal is HaLt2.
We prove the intermediate claim Hshift: add_SNo (minus_SNo asb) a < add_SNo (minus_SNo asb) (add_SNo s asb).
An exact proof term for the current goal is (add_SNo_Lt2 (minus_SNo asb) a (add_SNo s asb) (SNo_minus_SNo asb HasbS) HaS (SNo_add_SNo s asb HsS HasbS) HaLt3).
We prove the intermediate claim HlhsEq: add_SNo (minus_SNo asb) a = add_SNo a (minus_SNo asb).
An exact proof term for the current goal is (add_SNo_com (minus_SNo asb) a (SNo_minus_SNo asb HasbS) HaS).
We prove the intermediate claim HrhsEq0: add_SNo (minus_SNo asb) (add_SNo s asb) = add_SNo (add_SNo (minus_SNo asb) s) asb.
An exact proof term for the current goal is (add_SNo_assoc (minus_SNo asb) s asb (SNo_minus_SNo asb HasbS) HsS HasbS).
We prove the intermediate claim HrhsEq1: add_SNo (add_SNo (minus_SNo asb) s) asb = add_SNo (add_SNo s (minus_SNo asb)) asb.
rewrite the current goal using (add_SNo_com (minus_SNo asb) s (SNo_minus_SNo asb HasbS) HsS) (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim HrhsEq2: add_SNo (add_SNo s (minus_SNo asb)) asb = add_SNo s (add_SNo (minus_SNo asb) asb).
rewrite the current goal using (add_SNo_assoc s (minus_SNo asb) asb HsS (SNo_minus_SNo asb HasbS) HasbS) (from right to left).
Use reflexivity.
We prove the intermediate claim HrhsEq3: add_SNo (minus_SNo asb) asb = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_linv asb HasbS).
We prove the intermediate claim HrhsEq: add_SNo (minus_SNo asb) (add_SNo s asb) = s.
rewrite the current goal using HrhsEq0 (from left to right).
rewrite the current goal using HrhsEq1 (from left to right).
rewrite the current goal using HrhsEq2 (from left to right).
rewrite the current goal using HrhsEq3 (from left to right).
rewrite the current goal using (add_SNo_0R s HsS) (from left to right).
Use reflexivity.
We prove the intermediate claim HmulLt: mul_SNo a denS < s.
We prove the intermediate claim HmulDen: mul_SNo a denS = add_SNo a (minus_SNo asb).
rewrite the current goal using (mul_SNo_distrL a 1 (minus_SNo s) HaS SNo_1 (SNo_minus_SNo s HsS)) (from left to right).
rewrite the current goal using (mul_SNo_oneR a HaS) (from left to right) at position 1.
rewrite the current goal using (mul_SNo_minus_distrR a s HaS HsS) (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using HmulDen (from left to right).
rewrite the current goal using HlhsEq (from right to left) at position 1.
rewrite the current goal using HrhsEq (from right to left) at position 2.
An exact proof term for the current goal is Hshift.
We prove the intermediate claim HaltPsiS: a < div_SNo s denS.
An exact proof term for the current goal is (div_SNo_pos_LtR s denS a HsS HdenSS HaS HdenSpos HmulLt).
We prove the intermediate claim HaltPsi: Rlt a (apply_fun bounded_transform_psi s).
We prove the intermediate claim HdenSR: denS ∈ R.
An exact proof term for the current goal is (real_add_SNo 1 real_1 (minus_SNo s) (real_minus_SNo s HsR)).
rewrite the current goal using HpsiEq (from left to right).
An exact proof term for the current goal is (RltI a (div_SNo s denS) HaR (real_div_SNo s HsR denS HdenSR) HaltPsiS).
We prove the intermediate claim HrelA: order_rel R a (apply_fun bounded_transform_psi s).
An exact proof term for the current goal is (Rlt_implies_order_rel_R a (apply_fun bounded_transform_psi s) HaltPsi).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R a x0) (apply_fun bounded_transform_psi s) HpsiR HrelA).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (subspace_topologyI R R_standard_topology I (open_ray_upper R c) HrayOpen).
∎