Let f be given.

Assume Hf: f ∈ unbounded_sequences_Romega.

We prove the intermediate claim HfX: f ∈ X.

An exact proof term for the current goal is (SepE1 R_omega_space (λf0 : set ⇒ unbounded_sequence_Romega f0) f Hf).

We prove the intermediate claim Huf: unbounded_sequence_Romega f.

An exact proof term for the current goal is (SepE2 R_omega_space (λf0 : set ⇒ unbounded_sequence_Romega f0) f Hf).

We prove the intermediate claim H0omega: 0 ∈ ω.

An exact proof term for the current goal is (nat_p_omega 0 nat_0).

We prove the intermediate claim HX0: apply_fun Xi 0 = (R,R_standard_topology).

An exact proof term for the current goal is (const_space_family_apply ω R R_standard_topology 0 H0omega).

We prove the intermediate claim HT0: space_family_topology Xi 0 = R_standard_topology.

We prove the intermediate claim Hdef: space_family_topology Xi 0 = (apply_fun Xi 0) 1.

Use reflexivity.

rewrite the current goal using Hdef (from left to right).

rewrite the current goal using HX0 (from left to right).

An exact proof term for the current goal is (tuple_2_1_eq R R_standard_topology).

We prove the intermediate claim HTfam: R_standard_topology ∈ {space_family_topology Xi i|i ∈ ω}.

Apply ReplEq ω (λi : set ⇒ space_family_topology Xi i) R_standard_topology to the current goal.

Assume _ H2.

Apply H2 to the current goal.

We will prove ∃i ∈ ω, R_standard_topology = space_family_topology Xi i.

We use 0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is H0omega.

Use symmetry.

An exact proof term for the current goal is HT0.

We prove the intermediate claim Hm1R: minus_SNo 1 ∈ R.

An exact proof term for the current goal is (real_minus_SNo 1 real_1).

We prove the intermediate claim Hm1S: SNo (minus_SNo 1).

An exact proof term for the current goal is (real_SNo (minus_SNo 1) Hm1R).

We prove the intermediate claim Hm1lt1: minus_SNo 1 < 1.

An exact proof term for the current goal is (SNoLt_tra (minus_SNo 1) 0 1 Hm1S SNo_0 SNo_1 minus_1_lt_0 SNoLt_0_1).

Set U to be the term {(i,open_interval (add_SNo (apply_fun f i) (minus_SNo 1)) (add_SNo (apply_fun f i) 1))|i ∈ ω}.

Set bU to be the term {g ∈ X|∀i : set, i ∈ ω → apply_fun g i ∈ apply_fun U i}.

We prove the intermediate claim HUapply: ∀i : set, i ∈ ω → apply_fun U i = open_interval (add_SNo (apply_fun f i) (minus_SNo 1)) (add_SNo (apply_fun f i) 1).

Let i be given.

Assume Hi: i ∈ ω.

We will prove apply_fun U i = open_interval (add_SNo (apply_fun f i) (minus_SNo 1)) (add_SNo (apply_fun f i) 1).

We will prove Eps_i (λz ⇒ (i,z) ∈ U) = open_interval (add_SNo (apply_fun f i) (minus_SNo 1)) (add_SNo (apply_fun f i) 1).

We prove the intermediate claim H1: (i,open_interval (add_SNo (apply_fun f i) (minus_SNo 1)) (add_SNo (apply_fun f i) 1)) ∈ U.

An exact proof term for the current goal is (ReplI ω (λi0 : set ⇒ (i0,open_interval (add_SNo (apply_fun f i0) (minus_SNo 1)) (add_SNo (apply_fun f i0) 1))) i Hi).

We prove the intermediate claim H2: (i,Eps_i (λz ⇒ (i,z) ∈ U)) ∈ U.

An exact proof term for the current goal is (Eps_i_ax (λz ⇒ (i,z) ∈ U) (open_interval (add_SNo (apply_fun f i) (minus_SNo 1)) (add_SNo (apply_fun f i) 1)) H1).

Apply (ReplE_impred ω (λi0 : set ⇒ (i0,open_interval (add_SNo (apply_fun f i0) (minus_SNo 1)) (add_SNo (apply_fun f i0) 1))) (i,Eps_i (λz ⇒ (i,z) ∈ U)) H2) to the current goal.

Let i0 be given.

Assume Hi0: i0 ∈ ω.

Assume Heq: (i,Eps_i (λz ⇒ (i,z) ∈ U)) = (i0,open_interval (add_SNo (apply_fun f i0) (minus_SNo 1)) (add_SNo (apply_fun f i0) 1)).

We prove the intermediate claim Hi_eq: i = i0.

rewrite the current goal using (tuple_2_0_eq i (Eps_i (λz ⇒ (i,z) ∈ U))) (from right to left).

rewrite the current goal using (tuple_2_0_eq i0 (open_interval (add_SNo (apply_fun f i0) (minus_SNo 1)) (add_SNo (apply_fun f i0) 1))) (from right to left).

rewrite the current goal using Heq (from left to right).

Use reflexivity.

We prove the intermediate claim Hz_eq: Eps_i (λz ⇒ (i,z) ∈ U) = open_interval (add_SNo (apply_fun f i0) (minus_SNo 1)) (add_SNo (apply_fun f i0) 1).

rewrite the current goal using (tuple_2_1_eq i (Eps_i (λz ⇒ (i,z) ∈ U))) (from right to left).

rewrite the current goal using (tuple_2_1_eq i0 (open_interval (add_SNo (apply_fun f i0) (minus_SNo 1)) (add_SNo (apply_fun f i0) 1))) (from right to left).

rewrite the current goal using Heq (from left to right).

Use reflexivity.

rewrite the current goal using Hz_eq (from left to right).

rewrite the current goal using Hi_eq (from right to left).

Use reflexivity.

We use bU to witness the existential quantifier.

Apply andI to the current goal.

We will prove bU ∈ B.

We prove the intermediate claim HbUsub: bU ⊆ X.

Let g be given.

Assume Hg: g ∈ bU.

We will prove g ∈ X.

An exact proof term for the current goal is (SepE1 X (λg0 : set ⇒ ∀i : set, i ∈ ω → apply_fun g0 i ∈ apply_fun U i) g Hg).

We prove the intermediate claim HbUpow: bU ∈ 𝒫 X.

An exact proof term for the current goal is (PowerI X bU HbUsub).

We prove the intermediate claim HUfun: function_on U ω TU.

Let i be given.

Assume Hi: i ∈ ω.

We will prove apply_fun U i ∈ TU.

We prove the intermediate claim HfRi: apply_fun f i ∈ R.

An exact proof term for the current goal is (Romega_coord_in_R f i HfX Hi).

We prove the intermediate claim HfSi: SNo (apply_fun f i).

An exact proof term for the current goal is (real_SNo (apply_fun f i) HfRi).

We prove the intermediate claim HaR: add_SNo (apply_fun f i) (minus_SNo 1) ∈ R.

An exact proof term for the current goal is (real_add_SNo (apply_fun f i) HfRi (minus_SNo 1) Hm1R).

We prove the intermediate claim HbR: add_SNo (apply_fun f i) 1 ∈ R.

An exact proof term for the current goal is (real_add_SNo (apply_fun f i) HfRi 1 real_1).

We prove the intermediate claim HaS: SNo (add_SNo (apply_fun f i) (minus_SNo 1)).

An exact proof term for the current goal is (real_SNo (add_SNo (apply_fun f i) (minus_SNo 1)) HaR).

We prove the intermediate claim HbS: SNo (add_SNo (apply_fun f i) 1).

An exact proof term for the current goal is (real_SNo (add_SNo (apply_fun f i) 1) HbR).

We prove the intermediate claim Hlt: add_SNo (apply_fun f i) (minus_SNo 1) < add_SNo (apply_fun f i) 1.

An exact proof term for the current goal is (add_SNo_Lt2 (apply_fun f i) (minus_SNo 1) 1 HfSi Hm1S SNo_1 Hm1lt1).

We prove the intermediate claim HRlt: Rlt (add_SNo (apply_fun f i) (minus_SNo 1)) (add_SNo (apply_fun f i) 1).

An exact proof term for the current goal is (RltI (add_SNo (apply_fun f i) (minus_SNo 1)) (add_SNo (apply_fun f i) 1) HaR HbR Hlt).

We prove the intermediate claim HopenI: open_interval (add_SNo (apply_fun f i) (minus_SNo 1)) (add_SNo (apply_fun f i) 1) ∈ R_standard_topology.

An exact proof term for the current goal is (open_interval_in_R_standard_topology (add_SNo (apply_fun f i) (minus_SNo 1)) (add_SNo (apply_fun f i) 1) HRlt).

We prove the intermediate claim HappUi: apply_fun U i = open_interval (add_SNo (apply_fun f i) (minus_SNo 1)) (add_SNo (apply_fun f i) 1).

An exact proof term for the current goal is (HUapply i Hi).

rewrite the current goal using HappUi (from left to right).

An exact proof term for the current goal is (UnionI {space_family_topology Xi j|j ∈ ω} (open_interval (add_SNo (apply_fun f i) (minus_SNo 1)) (add_SNo (apply_fun f i) 1)) R_standard_topology HopenI HTfam).

We prove the intermediate claim HUtot: total_function_on U ω TU.

We prove the intermediate claim Htot': ∀i : set, i ∈ ω → ∃y : set, y ∈ TU ∧ (i,y) ∈ U.

Let i be given.

Assume Hi: i ∈ ω.

We use (apply_fun U i) to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (HUfun i Hi).

We prove the intermediate claim H1: (i,open_interval (add_SNo (apply_fun f i) (minus_SNo 1)) (add_SNo (apply_fun f i) 1)) ∈ U.

An exact proof term for the current goal is (ReplI ω (λi0 : set ⇒ (i0,open_interval (add_SNo (apply_fun f i0) (minus_SNo 1)) (add_SNo (apply_fun f i0) 1))) i Hi).

An exact proof term for the current goal is (Eps_i_ax (λz : set ⇒ (i,z) ∈ U) (open_interval (add_SNo (apply_fun f i) (minus_SNo 1)) (add_SNo (apply_fun f i) 1)) H1).

An exact proof term for the current goal is (andI (function_on U ω TU) (∀x : set, x ∈ ω → ∃y : set, y ∈ TU ∧ (x,y) ∈ U) HUfun Htot').

We prove the intermediate claim HUgraph: functional_graph U.

An exact proof term for the current goal is (functional_graph_graph ω (λi0 : set ⇒ open_interval (add_SNo (apply_fun f i0) (minus_SNo 1)) (add_SNo (apply_fun f i0) 1))).

We prove the intermediate claim HUcoords: ∀i : set, i ∈ ω → apply_fun U i ∈ space_family_topology Xi i.

Let i be given.

Assume Hi: i ∈ ω.

We will prove apply_fun U i ∈ space_family_topology Xi i.

We prove the intermediate claim HXi: apply_fun Xi i = (R,R_standard_topology).

An exact proof term for the current goal is (const_space_family_apply ω R R_standard_topology i Hi).

We prove the intermediate claim HTi: space_family_topology Xi i = R_standard_topology.

We prove the intermediate claim Hdef: space_family_topology Xi i = (apply_fun Xi i) 1.

Use reflexivity.

rewrite the current goal using Hdef (from left to right).

rewrite the current goal using HXi (from left to right).

An exact proof term for the current goal is (tuple_2_1_eq R R_standard_topology).

rewrite the current goal using HTi (from left to right).

We prove the intermediate claim HfRi: apply_fun f i ∈ R.

An exact proof term for the current goal is (Romega_coord_in_R f i HfX Hi).

We prove the intermediate claim HfSi: SNo (apply_fun f i).

An exact proof term for the current goal is (real_SNo (apply_fun f i) HfRi).

We prove the intermediate claim HaR: add_SNo (apply_fun f i) (minus_SNo 1) ∈ R.

An exact proof term for the current goal is (real_add_SNo (apply_fun f i) HfRi (minus_SNo 1) Hm1R).

We prove the intermediate claim HbR: add_SNo (apply_fun f i) 1 ∈ R.

An exact proof term for the current goal is (real_add_SNo (apply_fun f i) HfRi 1 real_1).

We prove the intermediate claim Hlt: add_SNo (apply_fun f i) (minus_SNo 1) < add_SNo (apply_fun f i) 1.

An exact proof term for the current goal is (add_SNo_Lt2 (apply_fun f i) (minus_SNo 1) 1 HfSi Hm1S SNo_1 Hm1lt1).

We prove the intermediate claim HRlt: Rlt (add_SNo (apply_fun f i) (minus_SNo 1)) (add_SNo (apply_fun f i) 1).

An exact proof term for the current goal is (RltI (add_SNo (apply_fun f i) (minus_SNo 1)) (add_SNo (apply_fun f i) 1) HaR HbR Hlt).

We prove the intermediate claim HopenI: open_interval (add_SNo (apply_fun f i) (minus_SNo 1)) (add_SNo (apply_fun f i) 1) ∈ R_standard_topology.

An exact proof term for the current goal is (open_interval_in_R_standard_topology (add_SNo (apply_fun f i) (minus_SNo 1)) (add_SNo (apply_fun f i) 1) HRlt).

We prove the intermediate claim HappUi: apply_fun U i = open_interval (add_SNo (apply_fun f i) (minus_SNo 1)) (add_SNo (apply_fun f i) 1).

An exact proof term for the current goal is (HUapply i Hi).

rewrite the current goal using HappUi (from left to right).

An exact proof term for the current goal is HopenI.

We prove the intermediate claim HexU: ∃U0 : set, total_function_on U0 ω TU ∧ functional_graph U0 ∧ (∀i : set, i ∈ ω → apply_fun U0 i ∈ space_family_topology Xi i) ∧ bU = {f0 ∈ X|∀i : set, i ∈ ω → apply_fun f0 i ∈ apply_fun U0 i}.

We use U to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HUtot.

An exact proof term for the current goal is HUgraph.

An exact proof term for the current goal is HUcoords.

Use reflexivity.

An exact proof term for the current goal is (SepI (𝒫 X) (λB0 : set ⇒ ∃U0 : set, total_function_on U0 ω TU ∧ functional_graph U0 ∧ (∀i : set, i ∈ ω → apply_fun U0 i ∈ space_family_topology Xi i) ∧ B0 = {f0 ∈ X|∀i : set, i ∈ ω → apply_fun f0 i ∈ apply_fun U0 i}) bU HbUpow HexU).

Apply andI to the current goal.

We will prove f ∈ bU.

Apply (SepI X (λg0 : set ⇒ ∀i : set, i ∈ ω → apply_fun g0 i ∈ apply_fun U i) f HfX) to the current goal.

Let i be given.

Assume Hi: i ∈ ω.

We will prove apply_fun f i ∈ apply_fun U i.

We prove the intermediate claim HfRi: apply_fun f i ∈ R.

An exact proof term for the current goal is (Romega_coord_in_R f i HfX Hi).

We prove the intermediate claim HfSi: SNo (apply_fun f i).

An exact proof term for the current goal is (real_SNo (apply_fun f i) HfRi).

We prove the intermediate claim HaR: add_SNo (apply_fun f i) (minus_SNo 1) ∈ R.

An exact proof term for the current goal is (real_add_SNo (apply_fun f i) HfRi (minus_SNo 1) Hm1R).

We prove the intermediate claim HbR: add_SNo (apply_fun f i) 1 ∈ R.

An exact proof term for the current goal is (real_add_SNo (apply_fun f i) HfRi 1 real_1).

We prove the intermediate claim Hx0eq: add_SNo (apply_fun f i) 0 = apply_fun f i.

An exact proof term for the current goal is (add_SNo_0R (apply_fun f i) HfSi).

We prove the intermediate claim Haxlt0: add_SNo (apply_fun f i) (minus_SNo 1) < add_SNo (apply_fun f i) 0.

An exact proof term for the current goal is (add_SNo_Lt2 (apply_fun f i) (minus_SNo 1) 0 HfSi Hm1S SNo_0 minus_1_lt_0).

We prove the intermediate claim Haxlt: add_SNo (apply_fun f i) (minus_SNo 1) < apply_fun f i.

rewrite the current goal using Hx0eq (from right to left) at position 2.

An exact proof term for the current goal is Haxlt0.

We prove the intermediate claim Hxltb0: add_SNo (apply_fun f i) 0 < add_SNo (apply_fun f i) 1.

An exact proof term for the current goal is (add_SNo_Lt2 (apply_fun f i) 0 1 HfSi SNo_0 SNo_1 SNoLt_0_1).

We prove the intermediate claim Hxltb: apply_fun f i < add_SNo (apply_fun f i) 1.

rewrite the current goal using Hx0eq (from right to left) at position 1.

An exact proof term for the current goal is Hxltb0.

We prove the intermediate claim HaRltx: Rlt (add_SNo (apply_fun f i) (minus_SNo 1)) (apply_fun f i).

An exact proof term for the current goal is (RltI (add_SNo (apply_fun f i) (minus_SNo 1)) (apply_fun f i) HaR HfRi Haxlt).

We prove the intermediate claim HxRltb: Rlt (apply_fun f i) (add_SNo (apply_fun f i) 1).

An exact proof term for the current goal is (RltI (apply_fun f i) (add_SNo (apply_fun f i) 1) HfRi HbR Hxltb).

We prove the intermediate claim HxIn: apply_fun f i ∈ open_interval (add_SNo (apply_fun f i) (minus_SNo 1)) (add_SNo (apply_fun f i) 1).

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt (add_SNo (apply_fun f i) (minus_SNo 1)) z ∧ Rlt z (add_SNo (apply_fun f i) 1)) (apply_fun f i) HfRi (andI (Rlt (add_SNo (apply_fun f i) (minus_SNo 1)) (apply_fun f i)) (Rlt (apply_fun f i) (add_SNo (apply_fun f i) 1)) HaRltx HxRltb)).

We prove the intermediate claim HappUi: apply_fun U i = open_interval (add_SNo (apply_fun f i) (minus_SNo 1)) (add_SNo (apply_fun f i) 1).

An exact proof term for the current goal is (HUapply i Hi).

rewrite the current goal using HappUi (from left to right).

An exact proof term for the current goal is HxIn.

Let g be given.

Assume Hg: g ∈ bU.

We will prove g ∈ unbounded_sequences_Romega.

We prove the intermediate claim HgX: g ∈ X.

An exact proof term for the current goal is (SepE1 X (λg0 : set ⇒ ∀i : set, i ∈ ω → apply_fun g0 i ∈ apply_fun U i) g Hg).

We prove the intermediate claim Hgprop: ∀i : set, i ∈ ω → apply_fun g i ∈ apply_fun U i.

An exact proof term for the current goal is (SepE2 X (λg0 : set ⇒ ∀i : set, i ∈ ω → apply_fun g0 i ∈ apply_fun U i) g Hg).

Apply (SepI R_omega_space (λh : set ⇒ unbounded_sequence_Romega h) g HgX) to the current goal.

We will prove unbounded_sequence_Romega g.

Let M be given.

Assume HM: M ∈ R.

Set K to be the term add_SNo M 1.

We prove the intermediate claim HKR: K ∈ R.

An exact proof term for the current goal is (real_add_SNo M HM 1 real_1).

We prove the intermediate claim Hexn: ∃n : set, n ∈ ω ∧ ¬ (apply_fun f n ∈ open_interval (minus_SNo K) K).

An exact proof term for the current goal is (Huf K HKR).

Apply Hexn to the current goal.

Let n be given.

Assume Hnconj.

We prove the intermediate claim HnO: n ∈ ω.

An exact proof term for the current goal is (andEL (n ∈ ω) (¬ (apply_fun f n ∈ open_interval (minus_SNo K) K)) Hnconj).

We prove the intermediate claim Hfnot: ¬ (apply_fun f n ∈ open_interval (minus_SNo K) K).

An exact proof term for the current goal is (andER (n ∈ ω) (¬ (apply_fun f n ∈ open_interval (minus_SNo K) K)) Hnconj).

We use n to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HnO.

We will prove ¬ (apply_fun g n ∈ open_interval (minus_SNo M) M).

Assume HgnIn: apply_fun g n ∈ open_interval (minus_SNo M) M.

We will prove False.

Apply Hfnot to the current goal.

We prove the intermediate claim HfnR: apply_fun f n ∈ R.

An exact proof term for the current goal is (Romega_coord_in_R f n HfX HnO).

We prove the intermediate claim HgnR: apply_fun g n ∈ R.

An exact proof term for the current goal is (Romega_coord_in_R g n HgX HnO).

We prove the intermediate claim HfnS: SNo (apply_fun f n).

An exact proof term for the current goal is (real_SNo (apply_fun f n) HfnR).

We prove the intermediate claim HgnS: SNo (apply_fun g n).

An exact proof term for the current goal is (real_SNo (apply_fun g n) HgnR).

We prove the intermediate claim HM_S: SNo M.

An exact proof term for the current goal is (real_SNo M HM).

We prove the intermediate claim HK_S: SNo K.

An exact proof term for the current goal is (real_SNo K HKR).

We prove the intermediate claim HgnBox: apply_fun g n ∈ open_interval (add_SNo (apply_fun f n) (minus_SNo 1)) (add_SNo (apply_fun f n) 1).

We prove the intermediate claim HgnU: apply_fun g n ∈ apply_fun U n.

An exact proof term for the current goal is (Hgprop n HnO).

We prove the intermediate claim HappUn: apply_fun U n = open_interval (add_SNo (apply_fun f n) (minus_SNo 1)) (add_SNo (apply_fun f n) 1).

An exact proof term for the current goal is (HUapply n HnO).

rewrite the current goal using HappUn (from right to left).

An exact proof term for the current goal is HgnU.

We prove the intermediate claim HgnInProp: Rlt (minus_SNo M) (apply_fun g n) ∧ Rlt (apply_fun g n) M.

An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt (minus_SNo M) z ∧ Rlt z M) (apply_fun g n) HgnIn).

We prove the intermediate claim Hgn_gt_mM: Rlt (minus_SNo M) (apply_fun g n).

An exact proof term for the current goal is (andEL (Rlt (minus_SNo M) (apply_fun g n)) (Rlt (apply_fun g n) M) HgnInProp).

We prove the intermediate claim Hgn_lt_M: Rlt (apply_fun g n) M.

An exact proof term for the current goal is (andER (Rlt (minus_SNo M) (apply_fun g n)) (Rlt (apply_fun g n) M) HgnInProp).

We prove the intermediate claim HgnBoxProp: Rlt (add_SNo (apply_fun f n) (minus_SNo 1)) (apply_fun g n) ∧ Rlt (apply_fun g n) (add_SNo (apply_fun f n) 1).

An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt (add_SNo (apply_fun f n) (minus_SNo 1)) z ∧ Rlt z (add_SNo (apply_fun f n) 1)) (apply_fun g n) HgnBox).

We prove the intermediate claim HxL_lt_y: Rlt (add_SNo (apply_fun f n) (minus_SNo 1)) (apply_fun g n).

An exact proof term for the current goal is (andEL (Rlt (add_SNo (apply_fun f n) (minus_SNo 1)) (apply_fun g n)) (Rlt (apply_fun g n) (add_SNo (apply_fun f n) 1)) HgnBoxProp).

We prove the intermediate claim Hy_lt_xR: Rlt (apply_fun g n) (add_SNo (apply_fun f n) 1).

An exact proof term for the current goal is (andER (Rlt (add_SNo (apply_fun f n) (minus_SNo 1)) (apply_fun g n)) (Rlt (apply_fun g n) (add_SNo (apply_fun f n) 1)) HgnBoxProp).

We prove the intermediate claim HxL_lt_y_lt: add_SNo (apply_fun f n) (minus_SNo 1) < apply_fun g n.

An exact proof term for the current goal is (RltE_lt (add_SNo (apply_fun f n) (minus_SNo 1)) (apply_fun g n) HxL_lt_y).

We prove the intermediate claim HxL1_lt_y1: add_SNo (add_SNo (apply_fun f n) (minus_SNo 1)) 1 < add_SNo (apply_fun g n) 1.

An exact proof term for the current goal is (add_SNo_Lt1 (add_SNo (apply_fun f n) (minus_SNo 1)) 1 (apply_fun g n) (SNo_add_SNo (apply_fun f n) (minus_SNo 1) HfnS Hm1S) SNo_1 HgnS HxL_lt_y_lt).

We prove the intermediate claim Hx_to_xL1: add_SNo (add_SNo (apply_fun f n) (minus_SNo 1)) 1 = apply_fun f n.

An exact proof term for the current goal is (add_SNo_minus_R2' (apply_fun f n) 1 HfnS SNo_1).

We prove the intermediate claim Hx_lt_y1_lt: apply_fun f n < add_SNo (apply_fun g n) 1.

rewrite the current goal using Hx_to_xL1 (from right to left) at position 1.

An exact proof term for the current goal is HxL1_lt_y1.

We prove the intermediate claim Hy1R: add_SNo (apply_fun g n) 1 ∈ R.

An exact proof term for the current goal is (real_add_SNo (apply_fun g n) HgnR 1 real_1).

We prove the intermediate claim Hx_lt_y1: Rlt (apply_fun f n) (add_SNo (apply_fun g n) 1).

An exact proof term for the current goal is (RltI (apply_fun f n) (add_SNo (apply_fun g n) 1) HfnR Hy1R Hx_lt_y1_lt).

We prove the intermediate claim Hy_lt_M_lt: apply_fun g n < M.

An exact proof term for the current goal is (RltE_lt (apply_fun g n) M Hgn_lt_M).

We prove the intermediate claim Hy1_lt_M1: add_SNo (apply_fun g n) 1 < add_SNo M 1.

An exact proof term for the current goal is (add_SNo_Lt1 (apply_fun g n) 1 M HgnS SNo_1 HM_S Hy_lt_M_lt).

We prove the intermediate claim Hy1_Rlt_K: Rlt (add_SNo (apply_fun g n) 1) K.

An exact proof term for the current goal is (RltI (add_SNo (apply_fun g n) 1) K Hy1R HKR Hy1_lt_M1).

We prove the intermediate claim Hx_lt_K: Rlt (apply_fun f n) K.

An exact proof term for the current goal is (Rlt_tra (apply_fun f n) (add_SNo (apply_fun g n) 1) K Hx_lt_y1 Hy1_Rlt_K).

We prove the intermediate claim Hy_gt_mM_lt: minus_SNo M < apply_fun g n.

An exact proof term for the current goal is (RltE_lt (minus_SNo M) (apply_fun g n) Hgn_gt_mM).

We prove the intermediate claim Hy_m1_lt_x: add_SNo (apply_fun g n) (minus_SNo 1) < apply_fun f n.

We prove the intermediate claim Hy_lt_xR_lt: apply_fun g n < add_SNo (apply_fun f n) 1.

An exact proof term for the current goal is (RltE_lt (apply_fun g n) (add_SNo (apply_fun f n) 1) Hy_lt_xR).

We prove the intermediate claim Hy_m1_lt_x0: add_SNo (apply_fun g n) (minus_SNo 1) < add_SNo (add_SNo (apply_fun f n) 1) (minus_SNo 1).

An exact proof term for the current goal is (add_SNo_Lt1 (apply_fun g n) (minus_SNo 1) (add_SNo (apply_fun f n) 1) HgnS Hm1S (SNo_add_SNo (apply_fun f n) 1 HfnS SNo_1) Hy_lt_xR_lt).

We prove the intermediate claim Hx1m1_eq: add_SNo (add_SNo (apply_fun f n) 1) (minus_SNo 1) = apply_fun f n.

An exact proof term for the current goal is (add_SNo_minus_R2 (apply_fun f n) 1 HfnS SNo_1).

rewrite the current goal using Hx1m1_eq (from right to left).

An exact proof term for the current goal is Hy_m1_lt_x0.

We prove the intermediate claim HmM_m1_lt_y_m1: add_SNo (minus_SNo M) (minus_SNo 1) < add_SNo (apply_fun g n) (minus_SNo 1).

An exact proof term for the current goal is (add_SNo_Lt1 (minus_SNo M) (minus_SNo 1) (apply_fun g n) (real_SNo (minus_SNo M) (real_minus_SNo M HM)) Hm1S HgnS Hy_gt_mM_lt).

We prove the intermediate claim HmM_m1_R: add_SNo (minus_SNo M) (minus_SNo 1) ∈ R.

An exact proof term for the current goal is (real_add_SNo (minus_SNo M) (real_minus_SNo M HM) (minus_SNo 1) Hm1R).

We prove the intermediate claim HKneg: minus_SNo K = add_SNo (minus_SNo M) (minus_SNo 1).

We prove the intermediate claim Hdist: minus_SNo (add_SNo M 1) = add_SNo (minus_SNo M) (minus_SNo 1).

An exact proof term for the current goal is (minus_add_SNo_distr M 1 (real_SNo M HM) SNo_1).

An exact proof term for the current goal is Hdist.

We prove the intermediate claim HmK_lt_x: Rlt (minus_SNo K) (apply_fun f n).

rewrite the current goal using HKneg (from left to right).

We prove the intermediate claim Htmp: Rlt (add_SNo (minus_SNo M) (minus_SNo 1)) (apply_fun f n).

We prove the intermediate claim Hmid: Rlt (add_SNo (minus_SNo M) (minus_SNo 1)) (add_SNo (apply_fun g n) (minus_SNo 1)).

An exact proof term for the current goal is (RltI (add_SNo (minus_SNo M) (minus_SNo 1)) (add_SNo (apply_fun g n) (minus_SNo 1)) HmM_m1_R (real_add_SNo (apply_fun g n) HgnR (minus_SNo 1) Hm1R) HmM_m1_lt_y_m1).

We prove the intermediate claim Hmid2: Rlt (add_SNo (apply_fun g n) (minus_SNo 1)) (apply_fun f n).

An exact proof term for the current goal is (RltI (add_SNo (apply_fun g n) (minus_SNo 1)) (apply_fun f n) (real_add_SNo (apply_fun g n) HgnR (minus_SNo 1) Hm1R) HfnR Hy_m1_lt_x).

An exact proof term for the current goal is (Rlt_tra (add_SNo (minus_SNo M) (minus_SNo 1)) (add_SNo (apply_fun g n) (minus_SNo 1)) (apply_fun f n) Hmid Hmid2).

An exact proof term for the current goal is Htmp.

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt (minus_SNo K) z ∧ Rlt z K) (apply_fun f n) HfnR (andI (Rlt (minus_SNo K) (apply_fun f n)) (Rlt (apply_fun f n) K) HmK_lt_x Hx_lt_K)).