Assume HabNe: ¬ (a = b).

We prove the intermediate claim HsepAx: ∀A0 B0 : set, closed_in X Tx A0 → closed_in X Tx B0 → A0 ∩ B0 = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A0 ⊆ U ∧ B0 ⊆ V ∧ U ∩ V = Empty.

An exact proof term for the current goal is (andER (one_point_sets_closed X Tx) (∀A0 B0 : set, closed_in X Tx A0 → closed_in X Tx B0 → A0 ∩ B0 = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A0 ⊆ U ∧ B0 ⊆ V ∧ U ∩ V = Empty) Hnorm).

We prove the intermediate claim HexShrink: ∃U0 V0 U1 V1 : set, (U0 ∈ Tx ∧ V0 ∈ Tx ∧ A ⊆ U0 ∧ B ⊆ V0 ∧ U0 ∩ V0 = Empty) ∧ ((U1 ∈ Tx ∧ A ⊆ U1 ∧ closure_of X Tx U1 ⊆ U0) ∧ (V1 ∈ Tx ∧ B ⊆ V1 ∧ closure_of X Tx V1 ⊆ V0)).

Apply (HsepAx A B HA HB Hdisj) to the current goal.

Let U0 be given.

Assume HexV0: ∃V0 : set, U0 ∈ Tx ∧ V0 ∈ Tx ∧ A ⊆ U0 ∧ B ⊆ V0 ∧ U0 ∩ V0 = Empty.

Apply HexV0 to the current goal.

Let V0 be given.

Assume HUV0: U0 ∈ Tx ∧ V0 ∈ Tx ∧ A ⊆ U0 ∧ B ⊆ V0 ∧ U0 ∩ V0 = Empty.

We prove the intermediate claim Hcore0: (((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ A ⊆ U0) ∧ B ⊆ V0).

An exact proof term for the current goal is (andEL (((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ A ⊆ U0) ∧ B ⊆ V0) (U0 ∩ V0 = Empty) HUV0).

We prove the intermediate claim Hcore1: ((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ A ⊆ U0).

An exact proof term for the current goal is (andEL ((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ A ⊆ U0) (B ⊆ V0) Hcore0).

We prove the intermediate claim HBsubV0: B ⊆ V0.

An exact proof term for the current goal is (andER ((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ A ⊆ U0) (B ⊆ V0) Hcore0).

We prove the intermediate claim HUVTx: (U0 ∈ Tx ∧ V0 ∈ Tx).

An exact proof term for the current goal is (andEL (U0 ∈ Tx ∧ V0 ∈ Tx) (A ⊆ U0) Hcore1).

We prove the intermediate claim HAsubU0: A ⊆ U0.

An exact proof term for the current goal is (andER (U0 ∈ Tx ∧ V0 ∈ Tx) (A ⊆ U0) Hcore1).

We prove the intermediate claim HU0Tx: U0 ∈ Tx.

An exact proof term for the current goal is (andEL (U0 ∈ Tx) (V0 ∈ Tx) HUVTx).

We prove the intermediate claim HV0Tx: V0 ∈ Tx.

An exact proof term for the current goal is (andER (U0 ∈ Tx) (V0 ∈ Tx) HUVTx).

We prove the intermediate claim HshrinkA: ∃U1 : set, U1 ∈ Tx ∧ A ⊆ U1 ∧ closure_of X Tx U1 ⊆ U0.

An exact proof term for the current goal is (normal_space_shrink_closed X Tx A U0 Hnorm HA HU0Tx HAsubU0).

Apply HshrinkA to the current goal.

Let U1 be given.

Assume HU1: U1 ∈ Tx ∧ A ⊆ U1 ∧ closure_of X Tx U1 ⊆ U0.

We prove the intermediate claim HshrinkB: ∃V1 : set, V1 ∈ Tx ∧ B ⊆ V1 ∧ closure_of X Tx V1 ⊆ V0.

An exact proof term for the current goal is (normal_space_shrink_closed X Tx B V0 Hnorm HB HV0Tx HBsubV0).

Apply HshrinkB to the current goal.

Let V1 be given.

Assume HV1: V1 ∈ Tx ∧ B ⊆ V1 ∧ closure_of X Tx V1 ⊆ V0.

We use U0 to witness the existential quantifier.

We use V0 to witness the existential quantifier.

We use U1 to witness the existential quantifier.

We use V1 to witness the existential quantifier.

We will prove (U0 ∈ Tx ∧ V0 ∈ Tx ∧ A ⊆ U0 ∧ B ⊆ V0 ∧ U0 ∩ V0 = Empty) ∧ ((U1 ∈ Tx ∧ A ⊆ U1 ∧ closure_of X Tx U1 ⊆ U0) ∧ (V1 ∈ Tx ∧ B ⊆ V1 ∧ closure_of X Tx V1 ⊆ V0)).

Apply andI to the current goal.

An exact proof term for the current goal is HUV0.

Apply andI to the current goal.

An exact proof term for the current goal is HU1.

An exact proof term for the current goal is HV1.

Apply HexShrink to the current goal.

Let U0 be given.

Assume HexV0: ∃V0 : set, ∃U1 : set, ∃V1 : set, (U0 ∈ Tx ∧ V0 ∈ Tx ∧ A ⊆ U0 ∧ B ⊆ V0 ∧ U0 ∩ V0 = Empty) ∧ ((U1 ∈ Tx ∧ A ⊆ U1 ∧ closure_of X Tx U1 ⊆ U0) ∧ (V1 ∈ Tx ∧ B ⊆ V1 ∧ closure_of X Tx V1 ⊆ V0)).

Apply HexV0 to the current goal.

Let V0 be given.

Assume HexU1: ∃U1 : set, ∃V1 : set, (U0 ∈ Tx ∧ V0 ∈ Tx ∧ A ⊆ U0 ∧ B ⊆ V0 ∧ U0 ∩ V0 = Empty) ∧ ((U1 ∈ Tx ∧ A ⊆ U1 ∧ closure_of X Tx U1 ⊆ U0) ∧ (V1 ∈ Tx ∧ B ⊆ V1 ∧ closure_of X Tx V1 ⊆ V0)).

Apply HexU1 to the current goal.

Let U1 be given.

Assume HexV1: ∃V1 : set, (U0 ∈ Tx ∧ V0 ∈ Tx ∧ A ⊆ U0 ∧ B ⊆ V0 ∧ U0 ∩ V0 = Empty) ∧ ((U1 ∈ Tx ∧ A ⊆ U1 ∧ closure_of X Tx U1 ⊆ U0) ∧ (V1 ∈ Tx ∧ B ⊆ V1 ∧ closure_of X Tx V1 ⊆ V0)).

Apply HexV1 to the current goal.

Let V1 be given.

Assume Hshrink: (U0 ∈ Tx ∧ V0 ∈ Tx ∧ A ⊆ U0 ∧ B ⊆ V0 ∧ U0 ∩ V0 = Empty) ∧ ((U1 ∈ Tx ∧ A ⊆ U1 ∧ closure_of X Tx U1 ⊆ U0) ∧ (V1 ∈ Tx ∧ B ⊆ V1 ∧ closure_of X Tx V1 ⊆ V0)).

We prove the intermediate claim HUV0: U0 ∈ Tx ∧ V0 ∈ Tx ∧ A ⊆ U0 ∧ B ⊆ V0 ∧ U0 ∩ V0 = Empty.

An exact proof term for the current goal is (andEL (U0 ∈ Tx ∧ V0 ∈ Tx ∧ A ⊆ U0 ∧ B ⊆ V0 ∧ U0 ∩ V0 = Empty) ((U1 ∈ Tx ∧ A ⊆ U1 ∧ closure_of X Tx U1 ⊆ U0) ∧ (V1 ∈ Tx ∧ B ⊆ V1 ∧ closure_of X Tx V1 ⊆ V0)) Hshrink).

We prove the intermediate claim HUV1: (U1 ∈ Tx ∧ A ⊆ U1 ∧ closure_of X Tx U1 ⊆ U0) ∧ (V1 ∈ Tx ∧ B ⊆ V1 ∧ closure_of X Tx V1 ⊆ V0).

An exact proof term for the current goal is (andER (U0 ∈ Tx ∧ V0 ∈ Tx ∧ A ⊆ U0 ∧ B ⊆ V0 ∧ U0 ∩ V0 = Empty) ((U1 ∈ Tx ∧ A ⊆ U1 ∧ closure_of X Tx U1 ⊆ U0) ∧ (V1 ∈ Tx ∧ B ⊆ V1 ∧ closure_of X Tx V1 ⊆ V0)) Hshrink).

We prove the intermediate claim HUV0core: (((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ A ⊆ U0) ∧ B ⊆ V0).

An exact proof term for the current goal is (andEL (((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ A ⊆ U0) ∧ B ⊆ V0) (U0 ∩ V0 = Empty) HUV0).

We prove the intermediate claim HUV0disj: U0 ∩ V0 = Empty.

An exact proof term for the current goal is (andER (((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ A ⊆ U0) ∧ B ⊆ V0) (U0 ∩ V0 = Empty) HUV0).

We prove the intermediate claim HUV0L: (U0 ∈ Tx ∧ V0 ∈ Tx) ∧ A ⊆ U0.

An exact proof term for the current goal is (andEL ((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ A ⊆ U0) (B ⊆ V0) HUV0core).

We prove the intermediate claim HBsubV0: B ⊆ V0.

An exact proof term for the current goal is (andER ((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ A ⊆ U0) (B ⊆ V0) HUV0core).

We prove the intermediate claim HUV0Tx: U0 ∈ Tx ∧ V0 ∈ Tx.

An exact proof term for the current goal is (andEL (U0 ∈ Tx ∧ V0 ∈ Tx) (A ⊆ U0) HUV0L).

We prove the intermediate claim HU0Tx: U0 ∈ Tx.

An exact proof term for the current goal is (andEL (U0 ∈ Tx) (V0 ∈ Tx) HUV0Tx).

We prove the intermediate claim HV0Tx: V0 ∈ Tx.

An exact proof term for the current goal is (andER (U0 ∈ Tx) (V0 ∈ Tx) HUV0Tx).

We prove the intermediate claim HUV1U: U1 ∈ Tx ∧ A ⊆ U1 ∧ closure_of X Tx U1 ⊆ U0.

An exact proof term for the current goal is (andEL (U1 ∈ Tx ∧ A ⊆ U1 ∧ closure_of X Tx U1 ⊆ U0) (V1 ∈ Tx ∧ B ⊆ V1 ∧ closure_of X Tx V1 ⊆ V0) HUV1).

We prove the intermediate claim HUV1V: V1 ∈ Tx ∧ B ⊆ V1 ∧ closure_of X Tx V1 ⊆ V0.

An exact proof term for the current goal is (andER (U1 ∈ Tx ∧ A ⊆ U1 ∧ closure_of X Tx U1 ⊆ U0) (V1 ∈ Tx ∧ B ⊆ V1 ∧ closure_of X Tx V1 ⊆ V0) HUV1).

We prove the intermediate claim HU1Tx: U1 ∈ Tx.

We prove the intermediate claim HU1pair: U1 ∈ Tx ∧ A ⊆ U1.

An exact proof term for the current goal is (andEL (U1 ∈ Tx ∧ A ⊆ U1) (closure_of X Tx U1 ⊆ U0) HUV1U).

An exact proof term for the current goal is (andEL (U1 ∈ Tx) (A ⊆ U1) HU1pair).

We prove the intermediate claim HV1Tx: V1 ∈ Tx.

We prove the intermediate claim HV1pair: V1 ∈ Tx ∧ B ⊆ V1.

An exact proof term for the current goal is (andEL (V1 ∈ Tx ∧ B ⊆ V1) (closure_of X Tx V1 ⊆ V0) HUV1V).

An exact proof term for the current goal is (andEL (V1 ∈ Tx) (B ⊆ V1) HV1pair).

We prove the intermediate claim HclU1subU0: closure_of X Tx U1 ⊆ U0.

An exact proof term for the current goal is (andER (U1 ∈ Tx ∧ A ⊆ U1) (closure_of X Tx U1 ⊆ U0) HUV1U).

We prove the intermediate claim HclV1subV0: closure_of X Tx V1 ⊆ V0.

An exact proof term for the current goal is (andER (V1 ∈ Tx ∧ B ⊆ V1) (closure_of X Tx V1 ⊆ V0) HUV1V).

We prove the intermediate claim HU1subX: U1 ⊆ X.

An exact proof term for the current goal is (topology_elem_subset X Tx U1 HTx HU1Tx).

We prove the intermediate claim HV1subX: V1 ⊆ X.

An exact proof term for the current goal is (topology_elem_subset X Tx V1 HTx HV1Tx).

We prove the intermediate claim HU1subU0: U1 ⊆ U0.

We prove the intermediate claim HU1subCl: U1 ⊆ closure_of X Tx U1.

An exact proof term for the current goal is (subset_of_closure X Tx U1 HTx HU1subX).

An exact proof term for the current goal is (Subq_tra U1 (closure_of X Tx U1) U0 HU1subCl HclU1subU0).

We prove the intermediate claim HV1subV0: V1 ⊆ V0.

We prove the intermediate claim HV1subCl: V1 ⊆ closure_of X Tx V1.

An exact proof term for the current goal is (subset_of_closure X Tx V1 HTx HV1subX).

An exact proof term for the current goal is (Subq_tra V1 (closure_of X Tx V1) V0 HV1subCl HclV1subV0).

We prove the intermediate claim HU1V1disj: U1 ∩ V1 = Empty.

Apply Empty_Subq_eq to the current goal.

We prove the intermediate claim HsubU0: U1 ∩ V1 ⊆ U0.

An exact proof term for the current goal is (Subq_tra (U1 ∩ V1) U1 U0 (binintersect_Subq_1 U1 V1) HU1subU0).

We prove the intermediate claim HsubV0: U1 ∩ V1 ⊆ V0.

An exact proof term for the current goal is (Subq_tra (U1 ∩ V1) V1 V0 (binintersect_Subq_2 U1 V1) HV1subV0).

We prove the intermediate claim HsubUV0: U1 ∩ V1 ⊆ U0 ∩ V0.

An exact proof term for the current goal is (binintersect_Subq_max U0 V0 (U1 ∩ V1) HsubU0 HsubV0).

We prove the intermediate claim HsubEmpty: U0 ∩ V0 ⊆ Empty.

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

An exact proof term for the current goal is (Subq_ref Empty).

An exact proof term for the current goal is (Subq_tra (U1 ∩ V1) (U0 ∩ V0) Empty HsubUV0 HsubEmpty).

We prove the intermediate claim HclU1clV1disj: closure_of X Tx U1 ∩ closure_of X Tx V1 = Empty.

Apply Empty_Subq_eq to the current goal.

We prove the intermediate claim HsubU0: closure_of X Tx U1 ∩ closure_of X Tx V1 ⊆ U0.

An exact proof term for the current goal is (Subq_tra (closure_of X Tx U1 ∩ closure_of X Tx V1) (closure_of X Tx U1) U0 (binintersect_Subq_1 (closure_of X Tx U1) (closure_of X Tx V1)) HclU1subU0).

We prove the intermediate claim HsubV0: closure_of X Tx U1 ∩ closure_of X Tx V1 ⊆ V0.

An exact proof term for the current goal is (Subq_tra (closure_of X Tx U1 ∩ closure_of X Tx V1) (closure_of X Tx V1) V0 (binintersect_Subq_2 (closure_of X Tx U1) (closure_of X Tx V1)) HclV1subV0).

We prove the intermediate claim HsubUV0: closure_of X Tx U1 ∩ closure_of X Tx V1 ⊆ U0 ∩ V0.

An exact proof term for the current goal is (binintersect_Subq_max U0 V0 (closure_of X Tx U1 ∩ closure_of X Tx V1) HsubU0 HsubV0).

We prove the intermediate claim HsubEmpty: U0 ∩ V0 ⊆ Empty.

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

An exact proof term for the current goal is (Subq_ref Empty).

An exact proof term for the current goal is (Subq_tra (closure_of X Tx U1 ∩ closure_of X Tx V1) (U0 ∩ V0) Empty HsubUV0 HsubEmpty).

We prove the intermediate claim Hnltba: ¬ (Rlt b a).

An exact proof term for the current goal is (RleE_nlt a b Hab).

We prove the intermediate claim HaRb: a ∈ R.

An exact proof term for the current goal is HaR.

We prove the intermediate claim HbRb: b ∈ R.

An exact proof term for the current goal is HbR.

We prove the intermediate claim Hltab: Rlt a b.

We prove the intermediate claim HaS: SNo a.

An exact proof term for the current goal is (real_SNo a HaRb).

We prove the intermediate claim HbS: SNo b.

An exact proof term for the current goal is (real_SNo b HbRb).

Apply (SNoLt_trichotomy_or_impred a b HaS HbS (Rlt a b)) to the current goal.

Assume HabSlt: a < b.

An exact proof term for the current goal is (RltI a b HaRb HbRb HabSlt).

Assume Heq: a = b.

Apply FalseE to the current goal.

An exact proof term for the current goal is (HabNe Heq).

Assume HbaSlt: b < a.

We prove the intermediate claim HbaRlt: Rlt b a.

An exact proof term for the current goal is (RltI b a HbRb HaRb HbaSlt).

Apply FalseE to the current goal.

An exact proof term for the current goal is (Hnltba HbaRlt).

Set U_b to be the term X ∖ B.

We prove the intermediate claim HU_bTx: U_b ∈ Tx.

An exact proof term for the current goal is (open_in_elem X Tx U_b (open_of_closed_complement X Tx B HB)).

We prove the intermediate claim HA_sub_U_b: A ⊆ U_b.

Let x be given.

Assume HxA: x ∈ A.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (HAsubX x HxA).

We prove the intermediate claim HxNotB: x ∉ B.

Assume HxB: x ∈ B.

We prove the intermediate claim HxAB: x ∈ A ∩ B.

An exact proof term for the current goal is (binintersectI A B x HxA HxB).

We prove the intermediate claim HxE: x ∈ Empty.

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

An exact proof term for the current goal is HxAB.

An exact proof term for the current goal is (EmptyE x HxE False).

An exact proof term for the current goal is (setminusI X B x HxX HxNotB).

We prove the intermediate claim HexU_a: ∃U_a : set, U_a ∈ Tx ∧ A ⊆ U_a ∧ closure_of X Tx U_a ⊆ U_b.

An exact proof term for the current goal is (normal_space_shrink_closed X Tx A U_b Hnorm HA HU_bTx HA_sub_U_b).

Apply HexU_a to the current goal.

Let U_a be given.

Assume HU_a: U_a ∈ Tx ∧ A ⊆ U_a ∧ closure_of X Tx U_a ⊆ U_b.

We prove the intermediate claim HU_aTx: U_a ∈ Tx.

We prove the intermediate claim HU_a12: U_a ∈ Tx ∧ A ⊆ U_a.

An exact proof term for the current goal is (andEL (U_a ∈ Tx ∧ A ⊆ U_a) (closure_of X Tx U_a ⊆ U_b) HU_a).

An exact proof term for the current goal is (andEL (U_a ∈ Tx) (A ⊆ U_a) HU_a12).

We prove the intermediate claim HclU_a_sub_U_b: closure_of X Tx U_a ⊆ U_b.

An exact proof term for the current goal is (andER (U_a ∈ Tx ∧ A ⊆ U_a) (closure_of X Tx U_a ⊆ U_b) HU_a).

We prove the intermediate claim Hex_between: ∀r : set, r ∈ R → Rlt a r → Rlt r b → ∃Ur : set, Ur ∈ Tx ∧ closure_of X Tx U_a ⊆ Ur ∧ closure_of X Tx Ur ⊆ U_b.

Let r be given.

Assume HrR: r ∈ R.

Assume Har: Rlt a r.

Assume Hrb: Rlt r b.

Set F to be the term UPair a b.

We prove the intermediate claim HFfin: finite F.

An exact proof term for the current goal is (finite_UPair a b).

We prove the intermediate claim HFsubR: F ⊆ R.

Let t be given.

Assume HtF: t ∈ F.

Apply (UPairE t a b HtF (t ∈ R)) to the current goal.

Assume Ht: t = a.

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

An exact proof term for the current goal is HaR.

Assume Ht: t = b.

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

An exact proof term for the current goal is HbR.

Set Uof to be the term (λt : set ⇒ if t = a then U_a else U_b).

We prove the intermediate claim HUof: ∀p : set, p ∈ F → Uof p ∈ Tx.

Let p be given.

Assume HpF: p ∈ F.

Apply (UPairE p a b HpF (Uof p ∈ Tx)) to the current goal.

Assume Hpa: p = a.

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

We prove the intermediate claim HUofbeta: Uof a = if a = a then U_a else U_b.

Use reflexivity.

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

We prove the intermediate claim Haa: a = a.

Use reflexivity.

rewrite the current goal using (If_i_1 (a = a) U_a U_b Haa) (from left to right).

An exact proof term for the current goal is HU_aTx.

Assume Hpb: p = b.

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

We prove the intermediate claim HUofbeta: Uof b = if b = a then U_a else U_b.

Use reflexivity.

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

We prove the intermediate claim Hbna: ¬ (b = a).

Assume Hba: b = a.

Apply HabNe to the current goal.

Use symmetry.

An exact proof term for the current goal is Hba.

rewrite the current goal using (If_i_0 (b = a) U_a U_b Hbna) (from left to right).

An exact proof term for the current goal is HU_bTx.

We prove the intermediate claim Hnest: ∀p q : set, p ∈ F → q ∈ F → Rlt p q → closure_of X Tx (Uof p) ⊆ Uof q.

Let p and q be given.

Assume HpF: p ∈ F.

Assume HqF: q ∈ F.

Assume Hpq: Rlt p q.

Apply (UPairE p a b HpF (closure_of X Tx (Uof p) ⊆ Uof q)) to the current goal.

Assume Hpa: p = a.

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

Apply (UPairE q a b HqF (closure_of X Tx (Uof a) ⊆ Uof q)) to the current goal.

Assume Hqa: q = a.

Apply FalseE to the current goal.

We prove the intermediate claim Haa: Rlt a a.

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

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

An exact proof term for the current goal is Hpq.

An exact proof term for the current goal is (not_Rlt_refl a HaR Haa).

Assume Hqb: q = b.

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

We prove the intermediate claim HUofa: Uof a = U_a.

We prove the intermediate claim Haa: a = a.

Use reflexivity.

We prove the intermediate claim HUofbeta: Uof a = if a = a then U_a else U_b.

Use reflexivity.

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

An exact proof term for the current goal is (If_i_1 (a = a) U_a U_b Haa).

We prove the intermediate claim HUofb: Uof b = U_b.

We prove the intermediate claim Hbna: ¬ (b = a).

Assume Hba: b = a.

Apply HabNe to the current goal.

Use symmetry.

An exact proof term for the current goal is Hba.

We prove the intermediate claim HUofbeta: Uof b = if b = a then U_a else U_b.

Use reflexivity.

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

An exact proof term for the current goal is (If_i_0 (b = a) U_a U_b Hbna).

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

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

An exact proof term for the current goal is HclU_a_sub_U_b.

Assume Hpb: p = b.

Apply FalseE to the current goal.

We prove the intermediate claim Hbq: Rlt b q.

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

An exact proof term for the current goal is Hpq.

Apply Hnltba to the current goal.

Apply (UPairE q a b HqF (Rlt b a)) to the current goal.

Assume Hqa: q = a.

We prove the intermediate claim Hba: Rlt b a.

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

An exact proof term for the current goal is Hbq.

An exact proof term for the current goal is Hba.

Assume Hqb: q = b.

Apply FalseE to the current goal.

We prove the intermediate claim Hbb: Rlt b b.

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

An exact proof term for the current goal is Hbq.

An exact proof term for the current goal is (not_Rlt_refl b HbR Hbb).

Apply (normal_extend_nested_open_family_by_point X Tx Hnorm F HFfin HFsubR Uof HUof Hnest r HrR) to the current goal.

Let Ur be given.

Assume HUr: Ur ∈ Tx ∧ (∀p0 : set, p0 ∈ F → Rlt p0 r → closure_of X Tx (Uof p0) ⊆ Ur) ∧ (∀q0 : set, q0 ∈ F → Rlt r q0 → closure_of X Tx Ur ⊆ Uof q0).

We use Ur to witness the existential quantifier.

We prove the intermediate claim HUr12: (Ur ∈ Tx ∧ ∀p0 : set, p0 ∈ F → Rlt p0 r → closure_of X Tx (Uof p0) ⊆ Ur).

An exact proof term for the current goal is (andEL (Ur ∈ Tx ∧ ∀p0 : set, p0 ∈ F → Rlt p0 r → closure_of X Tx (Uof p0) ⊆ Ur) (∀q0 : set, q0 ∈ F → Rlt r q0 → closure_of X Tx Ur ⊆ Uof q0) HUr).

We prove the intermediate claim HUrTx: Ur ∈ Tx.

An exact proof term for the current goal is (andEL (Ur ∈ Tx) (∀p0 : set, p0 ∈ F → Rlt p0 r → closure_of X Tx (Uof p0) ⊆ Ur) HUr12).

We prove the intermediate claim Hleft: ∀p0 : set, p0 ∈ F → Rlt p0 r → closure_of X Tx (Uof p0) ⊆ Ur.

An exact proof term for the current goal is (andER (Ur ∈ Tx) (∀p0 : set, p0 ∈ F → Rlt p0 r → closure_of X Tx (Uof p0) ⊆ Ur) HUr12).

We prove the intermediate claim Hright: ∀q0 : set, q0 ∈ F → Rlt r q0 → closure_of X Tx Ur ⊆ Uof q0.

An exact proof term for the current goal is (andER (Ur ∈ Tx ∧ ∀p0 : set, p0 ∈ F → Rlt p0 r → closure_of X Tx (Uof p0) ⊆ Ur) (∀q0 : set, q0 ∈ F → Rlt r q0 → closure_of X Tx Ur ⊆ Uof q0) HUr).

We prove the intermediate claim HUofa: Uof a = U_a.

We prove the intermediate claim Haa: a = a.

Use reflexivity.

We prove the intermediate claim HUofbeta: Uof a = if a = a then U_a else U_b.

Use reflexivity.

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

An exact proof term for the current goal is (If_i_1 (a = a) U_a U_b Haa).

We prove the intermediate claim HUofb: Uof b = U_b.

We prove the intermediate claim Hbna: ¬ (b = a).

Assume Hba: b = a.

Apply HabNe to the current goal.

Use symmetry.

An exact proof term for the current goal is Hba.

We prove the intermediate claim HUofbeta: Uof b = if b = a then U_a else U_b.

Use reflexivity.

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

An exact proof term for the current goal is (If_i_0 (b = a) U_a U_b Hbna).

Apply andI to the current goal.

An exact proof term for the current goal is HUrTx.

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

An exact proof term for the current goal is (Hleft a (UPairI1 a b) Har).

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

An exact proof term for the current goal is (Hright b (UPairI2 a b) Hrb).

Set P0 to be the term rational_numbers ∩ I.

Set P to be the term P0 ∪ (UPair a b).

We prove the intermediate claim HP_count: countable P.

We prove the intermediate claim HQcount: countable rational_numbers.

An exact proof term for the current goal is (rational_numbers_countable).

We prove the intermediate claim HP0count: countable P0.

An exact proof term for the current goal is (binintersect_countable_left rational_numbers I HQcount).

We prove the intermediate claim HabFin: finite (UPair a b).

An exact proof term for the current goal is (finite_UPair a b).

We prove the intermediate claim HabCount: countable (UPair a b).

An exact proof term for the current goal is (finite_countable (UPair a b) HabFin).

An exact proof term for the current goal is (binunion_countable P0 (UPair a b) HP0count HabCount).

We prove the intermediate claim HP_sub_R: P ⊆ R.

Let r be given.

Assume HrP: r ∈ P.

Apply (binunionE P0 (UPair a b) r HrP (r ∈ R)) to the current goal.

Assume HrP0: r ∈ P0.

We prove the intermediate claim HrQ: r ∈ rational_numbers.

An exact proof term for the current goal is (binintersectE1 rational_numbers I r HrP0).

An exact proof term for the current goal is (rational_numbers_in_R r HrQ).

Assume HrAB: r ∈ UPair a b.

We prove the intermediate claim HrEq: r = a ∨ r = b.

An exact proof term for the current goal is (UPairE r a b HrAB).

Apply HrEq to the current goal.

Assume Hra: r = a.

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

An exact proof term for the current goal is HaR.

Assume Hrb: r = b.

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

An exact proof term for the current goal is HbR.

Apply HP_count to the current goal.

Let code of type set → set be given.

Assume Hcode_inj: inj P ω code.

We prove the intermediate claim Hcode_in_omega: ∀p : set, p ∈ P → code p ∈ ω.

Apply Hcode_inj to the current goal.

Assume Hcode_in Hcode_inj0.

Let p be given.

Assume HpP: p ∈ P.

An exact proof term for the current goal is (Hcode_in p HpP).

Set Ppref to be the term (λn : set ⇒ {p ∈ P|code p ∈ ordsucc n}).

We prove the intermediate claim Hpref_finite: ∀n : set, nat_p n → finite (Ppref n).

Let n be given.

Assume Hnat: nat_p n.

An exact proof term for the current goal is (inj_omega_preimage_ordsucc_finite P n code Hnat Hcode_inj).

Set P_eq to be the term (λn : set ⇒ {p ∈ P|code p = n}).

Set pnew to be the term (λn : set ⇒ Eps_i (λp : set ⇒ p ∈ P ∧ code p = n)).

We prove the intermediate claim Hpnew_spec: ∀n : set, (∃p : set, p ∈ P ∧ code p = n) → pnew n ∈ P ∧ code (pnew n) = n.

Let n be given.

Assume Hex: ∃p : set, p ∈ P ∧ code p = n.

Set Ppred to be the term (λp : set ⇒ p ∈ P ∧ code p = n).

We prove the intermediate claim HpnewPpred: Ppred (pnew n).

An exact proof term for the current goal is (Eps_i_ex Ppred Hex).

An exact proof term for the current goal is HpnewPpred.

Set BaseF to be the term UPair a b.

Set BaseG to be the term graph BaseF (λt : set ⇒ if t = a then U_a else U_b).

Set BaseState to be the term (BaseF,BaseG).

Set Ur_of to be the term (λn st : set ⇒ Eps_i (λU : set ⇒ U ∈ Tx ∧ (∀p0 : set, p0 ∈ (st 0) → Rlt p0 (pnew n) → closure_of X Tx (apply_fun (st 1) p0) ⊆ U) ∧ (∀q0 : set, q0 ∈ (st 0) → Rlt (pnew n) q0 → closure_of X Tx U ⊆ apply_fun (st 1) q0))).

Set Gext to be the term (λn st : set ⇒ graph ((st 0) ∪ {pnew n}) (λp : set ⇒ if p = pnew n then Ur_of n st else apply_fun (st 1) p)).

Set StepState to be the term (λn st : set ⇒ if (∃p : set, p ∈ P ∧ code p = n) then if (pnew n ∈ (st 0)) then st else ((st 0) ∪ {pnew n},Gext n st) else st).

Set State to be the term (λn : set ⇒ nat_primrec BaseState StepState n).

Set Fof to be the term (λn : set ⇒ (State n) 0).

Set Gof to be the term (λn : set ⇒ (State n) 1).

Set Inv to be the term (λst : set ⇒ finite (st 0) ∧ (st 0 ⊆ R) ∧ total_function_on (st 1) (st 0) Tx ∧ functional_graph (st 1) ∧ graph_domain_subset (st 1) (st 0) ∧ ∀p q : set, p ∈ (st 0) → q ∈ (st 0) → Rlt p q → closure_of X Tx (apply_fun (st 1) p) ⊆ apply_fun (st 1) q).

We prove the intermediate claim HBaseFfin: finite BaseF.

An exact proof term for the current goal is (finite_UPair a b).

We prove the intermediate claim HBaseGa: apply_fun BaseG a = U_a.

We prove the intermediate claim HaBaseF: a ∈ BaseF.

An exact proof term for the current goal is (UPairI1 a b).

We prove the intermediate claim Haa: a = a.

Use reflexivity.

rewrite the current goal using (apply_fun_graph BaseF (λt : set ⇒ if t = a then U_a else U_b) a HaBaseF) (from left to right).

rewrite the current goal using (If_i_1 (a = a) U_a U_b Haa) (from left to right).

Use reflexivity.

We prove the intermediate claim HBaseGb: apply_fun BaseG b = U_b.

We prove the intermediate claim HbBaseF: b ∈ BaseF.

An exact proof term for the current goal is (UPairI2 a b).

rewrite the current goal using (apply_fun_graph BaseF (λt : set ⇒ if t = a then U_a else U_b) b HbBaseF) (from left to right).

We prove the intermediate claim Hbna: ¬ (b = a).

Assume Hba: b = a.

Apply HabNe to the current goal.

Use symmetry.

An exact proof term for the current goal is Hba.

rewrite the current goal using (If_i_0 (b = a) U_a U_b Hbna) (from left to right).

Use reflexivity.

We prove the intermediate claim HInvBase: Inv BaseState.

We prove the intermediate claim HBaseStateDef: BaseState = (BaseF,BaseG).

Use reflexivity.

We prove the intermediate claim HBaseState0: BaseState 0 = BaseF.

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

An exact proof term for the current goal is (tuple_2_0_eq BaseF BaseG).

We prove the intermediate claim HBaseState1: BaseState 1 = BaseG.

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

An exact proof term for the current goal is (tuple_2_1_eq BaseF BaseG).

We prove the intermediate claim HInvUnfold: Inv BaseState = (finite (BaseState 0) ∧ (BaseState 0 ⊆ R) ∧ total_function_on (BaseState 1) (BaseState 0) Tx ∧ functional_graph (BaseState 1) ∧ graph_domain_subset (BaseState 1) (BaseState 0) ∧ ∀p q : set, p ∈ (BaseState 0) → q ∈ (BaseState 0) → Rlt p q → closure_of X Tx (apply_fun (BaseState 1) p) ⊆ apply_fun (BaseState 1) q).

Use reflexivity.

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

Apply andI to the current goal.

We will prove (((finite (BaseState 0) ∧ (BaseState 0 ⊆ R)) ∧ total_function_on (BaseState 1) (BaseState 0) Tx) ∧ functional_graph (BaseState 1)) ∧ graph_domain_subset (BaseState 1) (BaseState 0).

Apply andI to the current goal.

We will prove ((finite (BaseState 0) ∧ (BaseState 0 ⊆ R)) ∧ total_function_on (BaseState 1) (BaseState 0) Tx) ∧ functional_graph (BaseState 1).

Apply andI to the current goal.

We will prove (finite (BaseState 0) ∧ (BaseState 0 ⊆ R)) ∧ total_function_on (BaseState 1) (BaseState 0) Tx.

Apply andI to the current goal.

We will prove finite (BaseState 0) ∧ (BaseState 0 ⊆ R).

Apply andI to the current goal.

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

An exact proof term for the current goal is HBaseFfin.

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

Let t be given.

Assume HtF: t ∈ BaseF.

Apply (UPairE t a b HtF (t ∈ R)) to the current goal.

Assume Hta: t = a.

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

An exact proof term for the current goal is HaR.

Assume Htb: t = b.

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

An exact proof term for the current goal is HbR.

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

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

Apply (total_function_on_graph BaseF Tx (λt : set ⇒ if t = a then U_a else U_b)) to the current goal.

Let t be given.

Assume HtF: t ∈ BaseF.

We prove the intermediate claim Ht_cases: t = a ∨ t = b.

An exact proof term for the current goal is (UPairE t a b HtF).

Apply Ht_cases to the current goal.

Assume Ht: t = a.

We prove the intermediate claim Hif: U_a = (λu : set ⇒ if u = a then U_a else U_b) t.

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

Use symmetry.

We prove the intermediate claim Haa: a = a.

Use reflexivity.

We prove the intermediate claim Hbeta: (λu : set ⇒ if u = a then U_a else U_b) a = if a = a then U_a else U_b.

Use reflexivity.

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

rewrite the current goal using (If_i_1 (a = a) U_a U_b Haa) (from left to right).

Use reflexivity.

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

An exact proof term for the current goal is HU_aTx.

Assume Ht: t = b.

We prove the intermediate claim Hbna: ¬ (b = a).

Assume Hba: b = a.

Apply HabNe to the current goal.

Use symmetry.

An exact proof term for the current goal is Hba.

We prove the intermediate claim Hif: U_b = (λu : set ⇒ if u = a then U_a else U_b) t.

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

Use symmetry.

We prove the intermediate claim Hbeta: (λu : set ⇒ if u = a then U_a else U_b) b = if b = a then U_a else U_b.

Use reflexivity.

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

rewrite the current goal using (If_i_0 (b = a) U_a U_b Hbna) (from left to right).

Use reflexivity.

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

An exact proof term for the current goal is HU_bTx.

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

An exact proof term for the current goal is (functional_graph_graph BaseF (λt : set ⇒ if t = a then U_a else U_b)).

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

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

An exact proof term for the current goal is (graph_domain_subset_graph BaseF (λt : set ⇒ if t = a then U_a else U_b)).

Let p and q be given.

Assume HpF: p ∈ (BaseState 0).

Assume HqF: q ∈ (BaseState 0).

Assume Hpq: Rlt p q.

We will prove closure_of X Tx (apply_fun (BaseState 1) p) ⊆ apply_fun (BaseState 1) q.

We prove the intermediate claim HpF0: p ∈ BaseF.

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

An exact proof term for the current goal is HpF.

We prove the intermediate claim HqF0: q ∈ BaseF.

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

An exact proof term for the current goal is HqF.

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

Apply (UPairE p a b HpF0 (closure_of X Tx (apply_fun BaseG p) ⊆ apply_fun BaseG q)) to the current goal.

Assume Hpa: p = a.

Apply (UPairE q a b HqF0 (closure_of X Tx (apply_fun BaseG p) ⊆ apply_fun BaseG q)) to the current goal.

Assume Hqa: q = a.

Apply FalseE to the current goal.

We prove the intermediate claim Hpqaa: Rlt a a.

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

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

An exact proof term for the current goal is Hpq.

An exact proof term for the current goal is ((not_Rlt_refl a HaR) Hpqaa).

Assume Hqb: q = b.

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

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

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

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

An exact proof term for the current goal is HclU_a_sub_U_b.

Assume Hpb: p = b.

Apply (UPairE q a b HqF0 (closure_of X Tx (apply_fun BaseG p) ⊆ apply_fun BaseG q)) to the current goal.

Assume Hqa: q = a.

Apply FalseE to the current goal.

We prove the intermediate claim Hpqba: Rlt b a.

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

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

An exact proof term for the current goal is Hpq.

An exact proof term for the current goal is (Hnltba Hpqba).

Assume Hqb: q = b.

Apply FalseE to the current goal.

We prove the intermediate claim Hpqbb: Rlt b b.

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

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

An exact proof term for the current goal is Hpq.

An exact proof term for the current goal is ((not_Rlt_refl b HbR) Hpqbb).

We prove the intermediate claim Hcode_inj_eq: ∀x z : set, x ∈ P → z ∈ P → code x = code z → x = z.

We prove the intermediate claim Hinj0: ∀x z ∈ P, code x = code z → x = z.

Apply Hcode_inj to the current goal.

Assume _ Hinj0'.

An exact proof term for the current goal is Hinj0'.

Let x be given.

Let z be given.

Assume HxP: x ∈ P.

Assume HzP: z ∈ P.

Assume Heq: code x = code z.

An exact proof term for the current goal is (Hinj0 x HxP z HzP Heq).

We prove the intermediate claim Hpnew_eq_of_code: ∀n p : set, p ∈ P → code p = n → (∃p0 : set, p0 ∈ P ∧ code p0 = n) → pnew n = p.

Let n and p be given.

Assume HpP: p ∈ P.

Assume Hcodep: code p = n.

Assume Hex: ∃p0 : set, p0 ∈ P ∧ code p0 = n.

We prove the intermediate claim Hpnewpair: pnew n ∈ P ∧ code (pnew n) = n.

An exact proof term for the current goal is (Hpnew_spec n Hex).

We prove the intermediate claim HpnewP: pnew n ∈ P.

An exact proof term for the current goal is (andEL (pnew n ∈ P) (code (pnew n) = n) Hpnewpair).

We prove the intermediate claim Hcodenew: code (pnew n) = n.

An exact proof term for the current goal is (andER (pnew n ∈ P) (code (pnew n) = n) Hpnewpair).

Apply (Hcode_inj_eq (pnew n) p HpnewP HpP) to the current goal.

We prove the intermediate claim Hcodeeq: code (pnew n) = code p.

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

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

Use reflexivity.

An exact proof term for the current goal is Hcodeeq.

We prove the intermediate claim HInvStep: ∀n st : set, Inv st → Inv (StepState n st).

Let n and st be given.

Assume HInvst: Inv st.

Apply (xm (∃p : set, p ∈ P ∧ code p = n)) to the current goal.

Assume Hex: ∃p : set, p ∈ P ∧ code p = n.

Apply (xm (pnew n ∈ (st 0))) to the current goal.

Assume Hin: pnew n ∈ (st 0).

We prove the intermediate claim Hbeta: StepState n st = if (∃p : set, p ∈ P ∧ code p = n) then (if (pnew n ∈ (st 0)) then st else ((st 0) ∪ {pnew n},Gext n st)) else st.

Use reflexivity.

We prove the intermediate claim Houter: StepState n st = if (pnew n ∈ (st 0)) then st else ((st 0) ∪ {pnew n},Gext n st).

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

An exact proof term for the current goal is (If_i_1 (∃p : set, p ∈ P ∧ code p = n) (if (pnew n ∈ (st 0)) then st else ((st 0) ∪ {pnew n},Gext n st)) st Hex).

We prove the intermediate claim Heq: StepState n st = st.

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

An exact proof term for the current goal is (If_i_1 (pnew n ∈ (st 0)) st ((st 0) ∪ {pnew n},Gext n st) Hin).

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

An exact proof term for the current goal is HInvst.

Assume Hnotin: ¬ (pnew n ∈ (st 0)).

We prove the intermediate claim Hbeta2: StepState n st = if (∃p : set, p ∈ P ∧ code p = n) then (if (pnew n ∈ (st 0)) then st else ((st 0) ∪ {pnew n},Gext n st)) else st.

Use reflexivity.

We prove the intermediate claim Houter2: StepState n st = if (pnew n ∈ (st 0)) then st else ((st 0) ∪ {pnew n},Gext n st).

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

An exact proof term for the current goal is (If_i_1 (∃p : set, p ∈ P ∧ code p = n) (if (pnew n ∈ (st 0)) then st else ((st 0) ∪ {pnew n},Gext n st)) st Hex).

We prove the intermediate claim Heq2: StepState n st = ((st 0) ∪ {pnew n},Gext n st).

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

An exact proof term for the current goal is (If_i_0 (pnew n ∈ (st 0)) st ((st 0) ∪ {pnew n},Gext n st) Hnotin).

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

We prove the intermediate claim HInvUnfold2: Inv st = (finite (st 0) ∧ (st 0 ⊆ R) ∧ total_function_on (st 1) (st 0) Tx ∧ functional_graph (st 1) ∧ graph_domain_subset (st 1) (st 0) ∧ ∀p q : set, p ∈ (st 0) → q ∈ (st 0) → Rlt p q → closure_of X Tx (apply_fun (st 1) p) ⊆ apply_fun (st 1) q).

Use reflexivity.

We prove the intermediate claim HInvStExp: finite (st 0) ∧ (st 0 ⊆ R) ∧ total_function_on (st 1) (st 0) Tx ∧ functional_graph (st 1) ∧ graph_domain_subset (st 1) (st 0) ∧ ∀p q : set, p ∈ (st 0) → q ∈ (st 0) → Rlt p q → closure_of X Tx (apply_fun (st 1) p) ⊆ apply_fun (st 1) q.

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

An exact proof term for the current goal is HInvst.

We prove the intermediate claim Hhead12345: ((((finite (st 0) ∧ (st 0 ⊆ R)) ∧ total_function_on (st 1) (st 0) Tx) ∧ functional_graph (st 1)) ∧ graph_domain_subset (st 1) (st 0)).

An exact proof term for the current goal is (andEL ((((finite (st 0) ∧ (st 0 ⊆ R)) ∧ total_function_on (st 1) (st 0) Tx) ∧ functional_graph (st 1)) ∧ graph_domain_subset (st 1) (st 0)) (∀p q : set, p ∈ (st 0) → q ∈ (st 0) → Rlt p q → closure_of X Tx (apply_fun (st 1) p) ⊆ apply_fun (st 1) q) HInvStExp).

We prove the intermediate claim Hnest: ∀p q : set, p ∈ (st 0) → q ∈ (st 0) → Rlt p q → closure_of X Tx (apply_fun (st 1) p) ⊆ apply_fun (st 1) q.

An exact proof term for the current goal is (andER ((((finite (st 0) ∧ (st 0 ⊆ R)) ∧ total_function_on (st 1) (st 0) Tx) ∧ functional_graph (st 1)) ∧ graph_domain_subset (st 1) (st 0)) (∀p q : set, p ∈ (st 0) → q ∈ (st 0) → Rlt p q → closure_of X Tx (apply_fun (st 1) p) ⊆ apply_fun (st 1) q) HInvStExp).

We prove the intermediate claim Hhead1234: (((finite (st 0) ∧ (st 0 ⊆ R)) ∧ total_function_on (st 1) (st 0) Tx) ∧ functional_graph (st 1)).

An exact proof term for the current goal is (andEL (((finite (st 0) ∧ (st 0 ⊆ R)) ∧ total_function_on (st 1) (st 0) Tx) ∧ functional_graph (st 1)) (graph_domain_subset (st 1) (st 0)) Hhead12345).

We prove the intermediate claim Hdom: graph_domain_subset (st 1) (st 0).

An exact proof term for the current goal is (andER (((finite (st 0) ∧ (st 0 ⊆ R)) ∧ total_function_on (st 1) (st 0) Tx) ∧ functional_graph (st 1)) (graph_domain_subset (st 1) (st 0)) Hhead12345).

We prove the intermediate claim Hhead123: ((finite (st 0) ∧ (st 0 ⊆ R)) ∧ total_function_on (st 1) (st 0) Tx).

An exact proof term for the current goal is (andEL ((finite (st 0) ∧ (st 0 ⊆ R)) ∧ total_function_on (st 1) (st 0) Tx) (functional_graph (st 1)) Hhead1234).

We prove the intermediate claim Hfun: functional_graph (st 1).

An exact proof term for the current goal is (andER ((finite (st 0) ∧ (st 0 ⊆ R)) ∧ total_function_on (st 1) (st 0) Tx) (functional_graph (st 1)) Hhead1234).

We prove the intermediate claim Hhead12: finite (st 0) ∧ (st 0 ⊆ R).

An exact proof term for the current goal is (andEL (finite (st 0) ∧ (st 0 ⊆ R)) (total_function_on (st 1) (st 0) Tx) Hhead123).

We prove the intermediate claim Htot: total_function_on (st 1) (st 0) Tx.

An exact proof term for the current goal is (andER (finite (st 0) ∧ (st 0 ⊆ R)) (total_function_on (st 1) (st 0) Tx) Hhead123).

We prove the intermediate claim HfinF: finite (st 0).

An exact proof term for the current goal is (andEL (finite (st 0)) (st 0 ⊆ R) Hhead12).

We prove the intermediate claim HFsubR0: st 0 ⊆ R.

An exact proof term for the current goal is (andER (finite (st 0)) (st 0 ⊆ R) Hhead12).

Set F to be the term (st 0).

Set Uof to be the term (λp : set ⇒ apply_fun (st 1) p).

We prove the intermediate claim HUofTx: ∀p : set, p ∈ F → Uof p ∈ Tx.

We prove the intermediate claim Hfunon: function_on (st 1) F Tx.

An exact proof term for the current goal is (andEL (function_on (st 1) F Tx) (∀x : set, x ∈ F → ∃y : set, y ∈ Tx ∧ (x,y) ∈ (st 1)) Htot).

Let p be given.

Assume HpF: p ∈ F.

An exact proof term for the current goal is (Hfunon p HpF).

We prove the intermediate claim HnestU: ∀p q : set, p ∈ F → q ∈ F → Rlt p q → closure_of X Tx (Uof p) ⊆ Uof q.

Let p and q be given.

Assume HpF: p ∈ F.

Assume HqF: q ∈ F.

Assume Hpq: Rlt p q.

An exact proof term for the current goal is (Hnest p q HpF HqF Hpq).

We prove the intermediate claim HrP: pnew n ∈ P.

An exact proof term for the current goal is (andEL (pnew n ∈ P) (code (pnew n) = n) (Hpnew_spec n Hex)).

We prove the intermediate claim HrR: pnew n ∈ R.

An exact proof term for the current goal is (HP_sub_R (pnew n) HrP).

We prove the intermediate claim HexU: ∃U : set, U ∈ Tx ∧ (∀p0 : set, p0 ∈ F → Rlt p0 (pnew n) → closure_of X Tx (Uof p0) ⊆ U) ∧ (∀q0 : set, q0 ∈ F → Rlt (pnew n) q0 → closure_of X Tx U ⊆ Uof q0).

An exact proof term for the current goal is (normal_extend_nested_open_family_by_point X Tx Hnorm F HfinF HFsubR0 Uof HUofTx HnestU (pnew n) HrR).

We prove the intermediate claim HUr_of: (Ur_of n st) ∈ Tx ∧ (∀p0 : set, p0 ∈ F → Rlt p0 (pnew n) → closure_of X Tx (Uof p0) ⊆ (Ur_of n st)) ∧ (∀q0 : set, q0 ∈ F → Rlt (pnew n) q0 → closure_of X Tx (Ur_of n st) ⊆ Uof q0).

Set Pred to be the term (λU : set ⇒ U ∈ Tx ∧ (∀p0 : set, p0 ∈ F → Rlt p0 (pnew n) → closure_of X Tx (Uof p0) ⊆ U) ∧ (∀q0 : set, q0 ∈ F → Rlt (pnew n) q0 → closure_of X Tx U ⊆ Uof q0)).

We prove the intermediate claim HexPred: ∃U : set, Pred U.

An exact proof term for the current goal is HexU.

An exact proof term for the current goal is (Eps_i_ex Pred HexPred).

We prove the intermediate claim HUr_head: (Ur_of n st) ∈ Tx ∧ (∀p0 : set, p0 ∈ F → Rlt p0 (pnew n) → closure_of X Tx (Uof p0) ⊆ (Ur_of n st)).

An exact proof term for the current goal is (andEL ((Ur_of n st) ∈ Tx ∧ (∀p0 : set, p0 ∈ F → Rlt p0 (pnew n) → closure_of X Tx (Uof p0) ⊆ (Ur_of n st))) (∀q0 : set, q0 ∈ F → Rlt (pnew n) q0 → closure_of X Tx (Ur_of n st) ⊆ Uof q0) HUr_of).

We prove the intermediate claim HUrTx: (Ur_of n st) ∈ Tx.

An exact proof term for the current goal is (andEL ((Ur_of n st) ∈ Tx) (∀p0 : set, p0 ∈ F → Rlt p0 (pnew n) → closure_of X Tx (Uof p0) ⊆ (Ur_of n st)) HUr_head).

We prove the intermediate claim HUrLower: ∀p0 : set, p0 ∈ F → Rlt p0 (pnew n) → closure_of X Tx (Uof p0) ⊆ (Ur_of n st).

An exact proof term for the current goal is (andER ((Ur_of n st) ∈ Tx) (∀p0 : set, p0 ∈ F → Rlt p0 (pnew n) → closure_of X Tx (Uof p0) ⊆ (Ur_of n st)) HUr_head).

We prove the intermediate claim HUrUpper: ∀q0 : set, q0 ∈ F → Rlt (pnew n) q0 → closure_of X Tx (Ur_of n st) ⊆ Uof q0.

An exact proof term for the current goal is (andER ((Ur_of n st) ∈ Tx ∧ (∀p0 : set, p0 ∈ F → Rlt p0 (pnew n) → closure_of X Tx (Uof p0) ⊆ (Ur_of n st))) (∀q0 : set, q0 ∈ F → Rlt (pnew n) q0 → closure_of X Tx (Ur_of n st) ⊆ Uof q0) HUr_of).

We prove the intermediate claim HInvUnfoldNew: Inv ((st 0) ∪ {pnew n},Gext n st) = (finite (((st 0) ∪ {pnew n},Gext n st) 0) ∧ (((st 0) ∪ {pnew n},Gext n st) 0 ⊆ R) ∧ total_function_on (((st 0) ∪ {pnew n},Gext n st) 1) (((st 0) ∪ {pnew n},Gext n st) 0) Tx ∧ functional_graph (((st 0) ∪ {pnew n},Gext n st) 1) ∧ graph_domain_subset (((st 0) ∪ {pnew n},Gext n st) 1) (((st 0) ∪ {pnew n},Gext n st) 0) ∧ ∀p q : set, p ∈ (((st 0) ∪ {pnew n},Gext n st) 0) → q ∈ (((st 0) ∪ {pnew n},Gext n st) 0) → Rlt p q → closure_of X Tx (apply_fun (((st 0) ∪ {pnew n},Gext n st) 1) p) ⊆ apply_fun (((st 0) ∪ {pnew n},Gext n st) 1) q).

Use reflexivity.

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

We prove the intermediate claim Htmp0: ((st 0) ∪ {pnew n},Gext n st) 0 = ((st 0) ∪ {pnew n}).

An exact proof term for the current goal is (tuple_2_0_eq ((st 0) ∪ {pnew n}) (Gext n st)).

We prove the intermediate claim Htmp1: ((st 0) ∪ {pnew n},Gext n st) 1 = (Gext n st).

An exact proof term for the current goal is (tuple_2_1_eq ((st 0) ∪ {pnew n}) (Gext n st)).

We prove the intermediate claim HFdef: (st 0) = F.

Use reflexivity.

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

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

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

We prove the intermediate claim HGextDef: Gext n st = graph (F ∪ {pnew n}) (λp : set ⇒ if p = pnew n then Ur_of n st else apply_fun (st 1) p).

Use reflexivity.

Apply andI to the current goal.

We will prove ((((finite (F ∪ {pnew n}) ∧ ((F ∪ {pnew n}) ⊆ R)) ∧ total_function_on (Gext n st) (F ∪ {pnew n}) Tx) ∧ functional_graph (Gext n st)) ∧ graph_domain_subset (Gext n st) (F ∪ {pnew n})).

Apply andI to the current goal.

We will prove (((finite (F ∪ {pnew n}) ∧ ((F ∪ {pnew n}) ⊆ R)) ∧ total_function_on (Gext n st) (F ∪ {pnew n}) Tx) ∧ functional_graph (Gext n st)).

Apply andI to the current goal.

We will prove ((finite (F ∪ {pnew n}) ∧ ((F ∪ {pnew n}) ⊆ R)) ∧ total_function_on (Gext n st) (F ∪ {pnew n}) Tx).

Apply andI to the current goal.

We will prove finite (F ∪ {pnew n}) ∧ ((F ∪ {pnew n}) ⊆ R).

Apply andI to the current goal.

An exact proof term for the current goal is (binunion_finite F HfinF {pnew n} (Sing_finite (pnew n))).

Let x be given.

Assume Hx: x ∈ (F ∪ {pnew n}).

We prove the intermediate claim Hx_cases: x ∈ F ∨ x ∈ {pnew n}.

An exact proof term for the current goal is (binunionE F {pnew n} x Hx).

Apply Hx_cases to the current goal.

Assume HxF: x ∈ F.

An exact proof term for the current goal is (HFsubR0 x HxF).

Assume Hxr: x ∈ {pnew n}.

We prove the intermediate claim Hxeq: x = pnew n.

An exact proof term for the current goal is (SingE (pnew n) x Hxr).

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

An exact proof term for the current goal is HrR.

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

Apply (total_function_on_graph (F ∪ {pnew n}) Tx (λp : set ⇒ if p = pnew n then Ur_of n st else apply_fun (st 1) p)) to the current goal.

Let p be given.

Assume Hp: p ∈ (F ∪ {pnew n}).

We prove the intermediate claim Hbeta_if: (λp0 : set ⇒ if p0 = pnew n then Ur_of n st else apply_fun (st 1) p0) p = (if p = pnew n then Ur_of n st else apply_fun (st 1) p).

Use reflexivity.

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

We prove the intermediate claim Hp_cases: p ∈ F ∨ p ∈ {pnew n}.

An exact proof term for the current goal is (binunionE F {pnew n} p Hp).

Apply Hp_cases to the current goal.

Assume HpF: p ∈ F.

Apply (xm (p = pnew n)) to the current goal.

Assume Heq: p = pnew n.

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

We prove the intermediate claim Hrfl: pnew n = pnew n.

Use reflexivity.

We prove the intermediate claim HIfEq1: (if pnew n = pnew n then Ur_of n st else apply_fun (st 1) (pnew n)) = Ur_of n st.

An exact proof term for the current goal is (If_i_1 (pnew n = pnew n) (Ur_of n st) (apply_fun (st 1) (pnew n)) Hrfl).

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

An exact proof term for the current goal is HUrTx.

Assume Hneq: ¬ (p = pnew n).

We prove the intermediate claim HIfEq: (if p = pnew n then Ur_of n st else apply_fun (st 1) p) = apply_fun (st 1) p.

An exact proof term for the current goal is (If_i_0 (p = pnew n) (Ur_of n st) (apply_fun (st 1) p) Hneq).

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

An exact proof term for the current goal is (HUofTx p HpF).

Assume Hpr: p ∈ {pnew n}.

We prove the intermediate claim Hpeq: p = pnew n.

An exact proof term for the current goal is (SingE (pnew n) p Hpr).

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

We prove the intermediate claim Hrfl: pnew n = pnew n.

Use reflexivity.

We prove the intermediate claim HIfEq1b: (if pnew n = pnew n then Ur_of n st else apply_fun (st 1) (pnew n)) = Ur_of n st.

An exact proof term for the current goal is (If_i_1 (pnew n = pnew n) (Ur_of n st) (apply_fun (st 1) (pnew n)) Hrfl).

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

An exact proof term for the current goal is HUrTx.

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

An exact proof term for the current goal is (functional_graph_graph (F ∪ {pnew n}) (λp : set ⇒ if p = pnew n then Ur_of n st else apply_fun (st 1) p)).

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

An exact proof term for the current goal is (graph_domain_subset_graph (F ∪ {pnew n}) (λp : set ⇒ if p = pnew n then Ur_of n st else apply_fun (st 1) p)).

Let p and q be given.

Assume Hp: p ∈ (F ∪ {pnew n}).

Assume Hq: q ∈ (F ∪ {pnew n}).

Assume Hpq: Rlt p q.

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

We prove the intermediate claim Hap_p: apply_fun (graph (F ∪ {pnew n}) (λp0 : set ⇒ if p0 = pnew n then Ur_of n st else apply_fun (st 1) p0)) p = (if p = pnew n then Ur_of n st else apply_fun (st 1) p).

An exact proof term for the current goal is (apply_fun_graph (F ∪ {pnew n}) (λp0 : set ⇒ if p0 = pnew n then Ur_of n st else apply_fun (st 1) p0) p Hp).

We prove the intermediate claim Hap_q: apply_fun (graph (F ∪ {pnew n}) (λp0 : set ⇒ if p0 = pnew n then Ur_of n st else apply_fun (st 1) p0)) q = (if q = pnew n then Ur_of n st else apply_fun (st 1) q).

An exact proof term for the current goal is (apply_fun_graph (F ∪ {pnew n}) (λp0 : set ⇒ if p0 = pnew n then Ur_of n st else apply_fun (st 1) p0) q Hq).

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

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

We prove the intermediate claim Hp_cases: p ∈ F ∨ p ∈ {pnew n}.

An exact proof term for the current goal is (binunionE F {pnew n} p Hp).

We prove the intermediate claim Hq_cases: q ∈ F ∨ q ∈ {pnew n}.

An exact proof term for the current goal is (binunionE F {pnew n} q Hq).

Apply Hp_cases to the current goal.

Assume HpF: p ∈ F.

Apply Hq_cases to the current goal.

Assume HqF: q ∈ F.

We prove the intermediate claim Hpneq: ¬ (p = pnew n).

Assume Heq: p = pnew n.

Apply Hnotin to the current goal.

We prove the intermediate claim HpnewInF: pnew n ∈ F.

We prove the intermediate claim Heq': pnew n = p.

Use symmetry.

An exact proof term for the current goal is Heq.

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

An exact proof term for the current goal is HpF.

An exact proof term for the current goal is HpnewInF.

We prove the intermediate claim Hqneq: ¬ (q = pnew n).

Assume Heq: q = pnew n.

Apply Hnotin to the current goal.

We prove the intermediate claim HpnewInF: pnew n ∈ F.

We prove the intermediate claim Heq': pnew n = q.

Use symmetry.

An exact proof term for the current goal is Heq.

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

An exact proof term for the current goal is HqF.

An exact proof term for the current goal is HpnewInF.

We prove the intermediate claim Hifp: (if p = pnew n then Ur_of n st else apply_fun (st 1) p) = apply_fun (st 1) p.

An exact proof term for the current goal is (If_i_0 (p = pnew n) (Ur_of n st) (apply_fun (st 1) p) Hpneq).

We prove the intermediate claim Hifq: (if q = pnew n then Ur_of n st else apply_fun (st 1) q) = apply_fun (st 1) q.

An exact proof term for the current goal is (If_i_0 (q = pnew n) (Ur_of n st) (apply_fun (st 1) q) Hqneq).

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

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

An exact proof term for the current goal is (Hnest p q HpF HqF Hpq).

Assume Hqr: q ∈ {pnew n}.

We prove the intermediate claim Hqeq: q = pnew n.

An exact proof term for the current goal is (SingE (pnew n) q Hqr).

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

We prove the intermediate claim Hrfl: pnew n = pnew n.

Use reflexivity.

We prove the intermediate claim Hifq: (if pnew n = pnew n then Ur_of n st else apply_fun (st 1) (pnew n)) = Ur_of n st.

An exact proof term for the current goal is (If_i_1 (pnew n = pnew n) (Ur_of n st) (apply_fun (st 1) (pnew n)) Hrfl).

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

We prove the intermediate claim Hpneq: ¬ (p = pnew n).

Assume Heq: p = pnew n.

Apply Hnotin to the current goal.

We prove the intermediate claim HpnewInF: pnew n ∈ F.

We prove the intermediate claim Heq': pnew n = p.

Use symmetry.

An exact proof term for the current goal is Heq.

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

An exact proof term for the current goal is HpF.

An exact proof term for the current goal is HpnewInF.

We prove the intermediate claim Hifp: (if p = pnew n then Ur_of n st else apply_fun (st 1) p) = apply_fun (st 1) p.

An exact proof term for the current goal is (If_i_0 (p = pnew n) (Ur_of n st) (apply_fun (st 1) p) Hpneq).

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

We prove the intermediate claim Hpq': Rlt p (pnew n).

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

An exact proof term for the current goal is Hpq.

An exact proof term for the current goal is (HUrLower p HpF Hpq').

Assume Hpr: p ∈ {pnew n}.

We prove the intermediate claim Hpeq: p = pnew n.

An exact proof term for the current goal is (SingE (pnew n) p Hpr).

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

Apply Hq_cases to the current goal.

Assume HqF: q ∈ F.

We prove the intermediate claim Hrfl: pnew n = pnew n.

Use reflexivity.

We prove the intermediate claim Hifp: (if pnew n = pnew n then Ur_of n st else apply_fun (st 1) (pnew n)) = Ur_of n st.

An exact proof term for the current goal is (If_i_1 (pnew n = pnew n) (Ur_of n st) (apply_fun (st 1) (pnew n)) Hrfl).

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

We prove the intermediate claim Hqneq: ¬ (q = pnew n).

Assume Heq: q = pnew n.

Apply Hnotin to the current goal.

We prove the intermediate claim HpnewInF: pnew n ∈ F.

We prove the intermediate claim Heq': pnew n = q.

Use symmetry.

An exact proof term for the current goal is Heq.

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

An exact proof term for the current goal is HqF.

An exact proof term for the current goal is HpnewInF.

We prove the intermediate claim Hifq: (if q = pnew n then Ur_of n st else apply_fun (st 1) q) = apply_fun (st 1) q.

An exact proof term for the current goal is (If_i_0 (q = pnew n) (Ur_of n st) (apply_fun (st 1) q) Hqneq).

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

We prove the intermediate claim Hpq': Rlt (pnew n) q.

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

An exact proof term for the current goal is Hpq.

An exact proof term for the current goal is (HUrUpper q HqF Hpq').

Assume Hqr: q ∈ {pnew n}.

We prove the intermediate claim Hqeq: q = pnew n.

An exact proof term for the current goal is (SingE (pnew n) q Hqr).

Apply FalseE to the current goal.

We prove the intermediate claim Hbad: Rlt (pnew n) (pnew n).

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

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

An exact proof term for the current goal is Hpq.

An exact proof term for the current goal is (not_Rlt_refl (pnew n) HrR Hbad).

Assume Hnone: ¬ (∃p : set, p ∈ P ∧ code p = n).

We prove the intermediate claim Hbeta: StepState n st = if (∃p : set, p ∈ P ∧ code p = n) then (if (pnew n ∈ (st 0)) then st else ((st 0) ∪ {pnew n},Gext n st)) else st.

Use reflexivity.

We prove the intermediate claim Heq: StepState n st = st.

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

An exact proof term for the current goal is (If_i_0 (∃p : set, p ∈ P ∧ code p = n) (if (pnew n ∈ (st 0)) then st else ((st 0) ∪ {pnew n},Gext n st)) st Hnone).

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

An exact proof term for the current goal is HInvst.

We prove the intermediate claim HInvAll: ∀n : set, nat_p n → Inv (State n).

Let n be given.

Assume HnNat: nat_p n.

We prove the intermediate claim Hbase: Inv (State 0).

We prove the intermediate claim H0: State 0 = BaseState.

An exact proof term for the current goal is (nat_primrec_0 BaseState StepState).

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

An exact proof term for the current goal is HInvBase.

We prove the intermediate claim Hstep: ∀k : set, nat_p k → Inv (State k) → Inv (State (ordsucc k)).

Let k be given.

Assume HkNat: nat_p k.

Assume HInvk: Inv (State k).

We prove the intermediate claim HS: State (ordsucc k) = StepState k (State k).

An exact proof term for the current goal is (nat_primrec_S BaseState StepState k HkNat).

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

An exact proof term for the current goal is (HInvStep k (State k) HInvk).

An exact proof term for the current goal is (nat_ind (λk : set ⇒ Inv (State k)) Hbase Hstep n HnNat).

Set U_Q to be the term (λp : set ⇒ if (Rlt p a) then Empty else (if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p)).

Set Qx to be the term (λx : set ⇒ {p ∈ rational_numbers|x ∈ U_Q p}).

Set LB to be the term (λx : set ⇒ {l ∈ R|∀p : set, p ∈ Qx x → p ∈ R → Rle l p}).

Set fx to be the term (λx : set ⇒ Eps_i (λr : set ⇒ R_lub (LB x) r)).

Set f to be the term graph X (λx : set ⇒ fx x).

We prove the intermediate claim Hp_in_dom_succ_code: ∀p : set, p ∈ P → p ∈ Fof (ordsucc (code p)).

Let p be given.

Assume HpP: p ∈ P.

Set n to be the term code p.

We prove the intermediate claim HnO: n ∈ ω.

An exact proof term for the current goal is (Hcode_in_omega p HpP).

We prove the intermediate claim HnNat: nat_p n.

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

We prove the intermediate claim HStS: State (ordsucc n) = StepState n (State n).

An exact proof term for the current goal is (nat_primrec_S BaseState StepState n HnNat).

We prove the intermediate claim Hex: ∃p0 : set, p0 ∈ P ∧ code p0 = n.

We use p to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HpP.

Use reflexivity.

We prove the intermediate claim Hcodep: code p = n.

Use reflexivity.

We prove the intermediate claim HpnewEq: pnew n = p.

An exact proof term for the current goal is (Hpnew_eq_of_code n p HpP Hcodep Hex).

Apply (xm (pnew n ∈ ((State n) 0))) to the current goal.

Assume Hin: pnew n ∈ ((State n) 0).

We prove the intermediate claim Hbeta: StepState n (State n) = if (∃p0 : set, p0 ∈ P ∧ code p0 = n) then (if (pnew n ∈ ((State n) 0)) then (State n) else (((State n) 0) ∪ {pnew n},Gext n (State n))) else (State n).

Use reflexivity.

We prove the intermediate claim Houter: StepState n (State n) = if (pnew n ∈ ((State n) 0)) then (State n) else (((State n) 0) ∪ {pnew n},Gext n (State n)).

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

An exact proof term for the current goal is (If_i_1 (∃p0 : set, p0 ∈ P ∧ code p0 = n) (if (pnew n ∈ ((State n) 0)) then (State n) else (((State n) 0) ∪ {pnew n},Gext n (State n))) (State n) Hex).

We prove the intermediate claim Heq: StepState n (State n) = State n.

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

An exact proof term for the current goal is (If_i_1 (pnew n ∈ ((State n) 0)) (State n) (((State n) 0) ∪ {pnew n},Gext n (State n)) Hin).

We prove the intermediate claim HFofDef: Fof (ordsucc n) = (State (ordsucc n)) 0.

Use reflexivity.

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

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

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

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

An exact proof term for the current goal is Hin.

Assume Hnotin: ¬ (pnew n ∈ ((State n) 0)).

Use reflexivity.

We prove the intermediate claim Houter: StepState n (State n) = if (pnew n ∈ ((State n) 0)) then (State n) else (((State n) 0) ∪ {pnew n},Gext n (State n)).

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

We prove the intermediate claim Heq: StepState n (State n) = (((State n) 0) ∪ {pnew n},Gext n (State n)).

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

An exact proof term for the current goal is (If_i_0 (pnew n ∈ ((State n) 0)) (State n) (((State n) 0) ∪ {pnew n},Gext n (State n)) Hnotin).

We prove the intermediate claim HFofDef: Fof (ordsucc n) = (State (ordsucc n)) 0.

Use reflexivity.

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

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

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

We prove the intermediate claim HpInSing: p ∈ {pnew n}.

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

An exact proof term for the current goal is (SingI p).

We prove the intermediate claim HdomEq: (((State n) 0) ∪ {pnew n},Gext n (State n)) 0 = ((State n) 0) ∪ {pnew n}.

An exact proof term for the current goal is (tuple_2_0_eq (((State n) 0) ∪ {pnew n}) (Gext n (State n))).

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

An exact proof term for the current goal is (binunionI2 ((State n) 0) {pnew n} p HpInSing).

We prove the intermediate claim Gof_preserve_old: ∀n p : set, nat_p n → p ∈ Fof n → apply_fun (Gof (ordsucc n)) p = apply_fun (Gof n) p.

Let n and p be given.

Assume HnNat: nat_p n.

Assume HpF: p ∈ Fof n.

We prove the intermediate claim HStS: State (ordsucc n) = StepState n (State n).

An exact proof term for the current goal is (nat_primrec_S BaseState StepState n HnNat).

Apply (xm (∃p0 : set, p0 ∈ P ∧ code p0 = n)) to the current goal.

Assume Hex: ∃p0 : set, p0 ∈ P ∧ code p0 = n.

Apply (xm (pnew n ∈ ((State n) 0))) to the current goal.

Assume Hin: pnew n ∈ ((State n) 0).

Use reflexivity.

We prove the intermediate claim Houter: StepState n (State n) = if (pnew n ∈ ((State n) 0)) then (State n) else (((State n) 0) ∪ {pnew n},Gext n (State n)).

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

We prove the intermediate claim Heq: StepState n (State n) = State n.

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

An exact proof term for the current goal is (If_i_1 (pnew n ∈ ((State n) 0)) (State n) (((State n) 0) ∪ {pnew n},Gext n (State n)) Hin).

We prove the intermediate claim HGofS: Gof (ordsucc n) = (State (ordsucc n)) 1.

Use reflexivity.

We prove the intermediate claim HGofN: Gof n = (State n) 1.

Use reflexivity.

We prove the intermediate claim HStS1: (State (ordsucc n)) 1 = (StepState n (State n)) 1.

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

Use reflexivity.

We prove the intermediate claim Heq1: (StepState n (State n)) 1 = (State n) 1.

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

Use reflexivity.

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

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

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

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

Use reflexivity.

Assume Hnotin: ¬ (pnew n ∈ ((State n) 0)).

Use reflexivity.

We prove the intermediate claim Houter: StepState n (State n) = if (pnew n ∈ ((State n) 0)) then (State n) else (((State n) 0) ∪ {pnew n},Gext n (State n)).

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

We prove the intermediate claim Heq: StepState n (State n) = (((State n) 0) ∪ {pnew n},Gext n (State n)).

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

An exact proof term for the current goal is (If_i_0 (pnew n ∈ ((State n) 0)) (State n) (((State n) 0) ∪ {pnew n},Gext n (State n)) Hnotin).

We prove the intermediate claim HGofS: Gof (ordsucc n) = (State (ordsucc n)) 1.

Use reflexivity.

We prove the intermediate claim HGofN: Gof n = (State n) 1.

Use reflexivity.

We prove the intermediate claim HStS1: (State (ordsucc n)) 1 = (StepState n (State n)) 1.

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

Use reflexivity.

We prove the intermediate claim Heq1: (StepState n (State n)) 1 = Gext n (State n).

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

An exact proof term for the current goal is (tuple_2_1_eq (((State n) 0) ∪ {pnew n}) (Gext n (State n))).

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

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

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

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

We prove the intermediate claim HpDom': p ∈ ((State n) 0 ∪ {pnew n}).

An exact proof term for the current goal is (binunionI1 ((State n) 0) {pnew n} p HpF).

We prove the intermediate claim HpNe: ¬ (p = pnew n).

Assume HpEq: p = pnew n.

We prove the intermediate claim HpnewF: pnew n ∈ Fof n.

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

An exact proof term for the current goal is HpF.

We prove the intermediate claim HFofDef: Fof n = (State n) 0.

Use reflexivity.

We prove the intermediate claim HpnewDom: pnew n ∈ ((State n) 0).

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

An exact proof term for the current goal is HpnewF.

Apply Hnotin to the current goal.

An exact proof term for the current goal is HpnewDom.

We prove the intermediate claim HGextDef: Gext n (State n) = graph ((State n) 0 ∪ {pnew n}) (λq : set ⇒ if q = pnew n then Ur_of n (State n) else apply_fun ((State n) 1) q).

Use reflexivity.

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

Set gextfun to be the term (λq : set ⇒ if q = pnew n then Ur_of n (State n) else apply_fun ((State n) 1) q).

We prove the intermediate claim Happ: apply_fun (graph ((State n) 0 ∪ {pnew n}) gextfun) p = gextfun p.

An exact proof term for the current goal is (apply_fun_graph ((State n) 0 ∪ {pnew n}) gextfun p HpDom').

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

We prove the intermediate claim Hgextfunp: gextfun p = (if p = pnew n then Ur_of n (State n) else apply_fun ((State n) 1) p).

Use reflexivity.

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

We prove the intermediate claim Hif: (if p = pnew n then Ur_of n (State n) else apply_fun ((State n) 1) p) = apply_fun ((State n) 1) p.

An exact proof term for the current goal is (If_i_0 (p = pnew n) (Ur_of n (State n)) (apply_fun ((State n) 1) p) HpNe).

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

Use reflexivity.

Assume Hnone: ¬ (∃p0 : set, p0 ∈ P ∧ code p0 = n).

Use reflexivity.

We prove the intermediate claim Heq: StepState n (State n) = State n.

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

An exact proof term for the current goal is (If_i_0 (∃p0 : set, p0 ∈ P ∧ code p0 = n) (if (pnew n ∈ ((State n) 0)) then (State n) else (((State n) 0) ∪ {pnew n},Gext n (State n))) (State n) Hnone).

We prove the intermediate claim HGofS: Gof (ordsucc n) = (State (ordsucc n)) 1.

Use reflexivity.

We prove the intermediate claim HGofN: Gof n = (State n) 1.

Use reflexivity.

We prove the intermediate claim HStS1: (State (ordsucc n)) 1 = (StepState n (State n)) 1.

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

Use reflexivity.

We prove the intermediate claim Heq1: (StepState n (State n)) 1 = (State n) 1.

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

Use reflexivity.

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

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

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

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

Use reflexivity.

We prove the intermediate claim Fof_mono_succ: ∀n : set, nat_p n → Fof n ⊆ Fof (ordsucc n).

Let n be given.

Assume HnNat: nat_p n.

Let p be given.

Assume HpF: p ∈ Fof n.

We will prove p ∈ Fof (ordsucc n).

We prove the intermediate claim HFofS: Fof (ordsucc n) = (State (ordsucc n)) 0.

Use reflexivity.

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

We prove the intermediate claim HStS: State (ordsucc n) = StepState n (State n).

An exact proof term for the current goal is (nat_primrec_S BaseState StepState n HnNat).

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

Apply (xm (∃p0 : set, p0 ∈ P ∧ code p0 = n)) to the current goal.

Assume Hex: ∃p0 : set, p0 ∈ P ∧ code p0 = n.

Apply (xm (pnew n ∈ ((State n) 0))) to the current goal.

Assume Hin: pnew n ∈ ((State n) 0).

Use reflexivity.

We prove the intermediate claim Houter: StepState n (State n) = if (pnew n ∈ ((State n) 0)) then (State n) else (((State n) 0) ∪ {pnew n},Gext n (State n)).

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

We prove the intermediate claim Heq: StepState n (State n) = State n.

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

An exact proof term for the current goal is (If_i_1 (pnew n ∈ ((State n) 0)) (State n) (((State n) 0) ∪ {pnew n},Gext n (State n)) Hin).

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

We prove the intermediate claim HFofN: Fof n = (State n) 0.

Use reflexivity.

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

An exact proof term for the current goal is HpF.

Assume Hnotin: ¬ (pnew n ∈ ((State n) 0)).

Use reflexivity.

We prove the intermediate claim Houter: StepState n (State n) = if (pnew n ∈ ((State n) 0)) then (State n) else (((State n) 0) ∪ {pnew n},Gext n (State n)).

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

We prove the intermediate claim Heq: StepState n (State n) = (((State n) 0) ∪ {pnew n},Gext n (State n)).

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

An exact proof term for the current goal is (If_i_0 (pnew n ∈ ((State n) 0)) (State n) (((State n) 0) ∪ {pnew n},Gext n (State n)) Hnotin).

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

We prove the intermediate claim HdomEq: (((State n) 0) ∪ {pnew n},Gext n (State n)) 0 = ((State n) 0) ∪ {pnew n}.

An exact proof term for the current goal is (tuple_2_0_eq (((State n) 0) ∪ {pnew n}) (Gext n (State n))).

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

We prove the intermediate claim HFofN: Fof n = (State n) 0.

Use reflexivity.

We prove the intermediate claim HpDom: p ∈ ((State n) 0).

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

An exact proof term for the current goal is HpF.

An exact proof term for the current goal is (binunionI1 ((State n) 0) {pnew n} p HpDom).

Assume Hnone: ¬ (∃p0 : set, p0 ∈ P ∧ code p0 = n).

Use reflexivity.

We prove the intermediate claim Heq: StepState n (State n) = State n.

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

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

We prove the intermediate claim HFofN: Fof n = (State n) 0.

Use reflexivity.

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

An exact proof term for the current goal is HpF.

We prove the intermediate claim Fof_increase_by_add: ∀n k p : set, nat_p n → nat_p k → p ∈ Fof n → p ∈ Fof (add_nat n k).

Let n, k and p be given.

Assume HnNat: nat_p n.

Assume HkNat: nat_p k.

Assume HpF: p ∈ Fof n.

We prove the intermediate claim Hbase: p ∈ Fof (add_nat n 0).

We prove the intermediate claim Hadd0: add_nat n 0 = n.

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

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

An exact proof term for the current goal is HpF.

We prove the intermediate claim Hstep: ∀t : set, nat_p t → (p ∈ Fof (add_nat n t)) → p ∈ Fof (add_nat n (ordsucc t)).

Let t be given.

Assume HtNat: nat_p t.

Assume HtIH: p ∈ Fof (add_nat n t).

We prove the intermediate claim HaddS: add_nat n (ordsucc t) = ordsucc (add_nat n t).

An exact proof term for the current goal is (add_nat_SR n t HtNat).

We prove the intermediate claim HntNat: nat_p (add_nat n t).

An exact proof term for the current goal is (add_nat_p n HnNat t HtNat).

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

An exact proof term for the current goal is (Fof_mono_succ (add_nat n t) HntNat p HtIH).

An exact proof term for the current goal is (nat_ind (λt : set ⇒ p ∈ Fof (add_nat n t)) Hbase Hstep k HkNat).

We prove the intermediate claim Gof_preserve_add: ∀n k p : set, nat_p n → nat_p k → p ∈ Fof n → apply_fun (Gof (add_nat n k)) p = apply_fun (Gof n) p.

Let n, k and p be given.

Assume HnNat: nat_p n.

Assume HkNat: nat_p k.

Assume HpF: p ∈ Fof n.

We prove the intermediate claim Hbase: apply_fun (Gof (add_nat n 0)) p = apply_fun (Gof n) p.

We prove the intermediate claim Hadd0: add_nat n 0 = n.

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

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

Use reflexivity.

We prove the intermediate claim Hstep: ∀t : set, nat_p t → (apply_fun (Gof (add_nat n t)) p = apply_fun (Gof n) p) → (apply_fun (Gof (add_nat n (ordsucc t))) p = apply_fun (Gof n) p).

Let t be given.

Assume HtNat: nat_p t.

Assume HtIH: apply_fun (Gof (add_nat n t)) p = apply_fun (Gof n) p.

We prove the intermediate claim HaddS: add_nat n (ordsucc t) = ordsucc (add_nat n t).

An exact proof term for the current goal is (add_nat_SR n t HtNat).

We prove the intermediate claim HntNat: nat_p (add_nat n t).

An exact proof term for the current goal is (add_nat_p n HnNat t HtNat).

We prove the intermediate claim HpFnt: p ∈ Fof (add_nat n t).

An exact proof term for the current goal is (Fof_increase_by_add n t p HnNat HtNat HpF).

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

We prove the intermediate claim Hpres: apply_fun (Gof (ordsucc (add_nat n t))) p = apply_fun (Gof (add_nat n t)) p.

An exact proof term for the current goal is (Gof_preserve_old (add_nat n t) p HntNat HpFnt).

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

An exact proof term for the current goal is HtIH.

An exact proof term for the current goal is (nat_ind (λt : set ⇒ apply_fun (Gof (add_nat n t)) p = apply_fun (Gof n) p) Hbase Hstep k HkNat).

We prove the intermediate claim Inv_nesting_at: ∀n p q : set, nat_p n → p ∈ Fof n → q ∈ Fof n → Rlt p q → closure_of X Tx (apply_fun (Gof n) p) ⊆ apply_fun (Gof n) q.

Let n, p and q be given.

Assume HnNat: nat_p n.

Assume HpF: p ∈ Fof n.

Assume HqF: q ∈ Fof n.

Assume Hpq: Rlt p q.

We prove the intermediate claim HInvStage: Inv (State n).

An exact proof term for the current goal is (HInvAll n HnNat).

Apply (and6E (finite ((State n) 0)) (((State n) 0 ⊆ R)) (total_function_on ((State n) 1) ((State n) 0) Tx) (functional_graph ((State n) 1)) (graph_domain_subset ((State n) 1) ((State n) 0)) (∀p0 q0 : set, p0 ∈ ((State n) 0) → q0 ∈ ((State n) 0) → Rlt p0 q0 → closure_of X Tx (apply_fun ((State n) 1) p0) ⊆ apply_fun ((State n) 1) q0) HInvStage (closure_of X Tx (apply_fun (Gof n) p) ⊆ apply_fun (Gof n) q)) to the current goal.

Assume Hfin Hsub Htot Hfg Hgd Hnest.

We prove the intermediate claim HFofDef: Fof n = (State n) 0.

Use reflexivity.

We prove the intermediate claim HGofDef: Gof n = (State n) 1.

Use reflexivity.

We prove the intermediate claim HpDom: p ∈ ((State n) 0).

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

An exact proof term for the current goal is HpF.

We prove the intermediate claim HqDom: q ∈ ((State n) 0).

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

An exact proof term for the current goal is HqF.

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

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

An exact proof term for the current goal is (Hnest p q HpDom HqDom Hpq).

We prove the intermediate claim U_Q_closure_mono_I: ∀p q : set, p ∈ rational_numbers → q ∈ rational_numbers → p ∈ I → q ∈ I → Rlt p q → closure_of X Tx (U_Q p) ⊆ U_Q q.

Let p and q be given.

Assume HpQ: p ∈ rational_numbers.

Assume HqQ: q ∈ rational_numbers.

Assume HpI: p ∈ I.

Assume HqI: q ∈ I.

Assume Hpq: Rlt p q.

We prove the intermediate claim HpR: p ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R p HpQ).

We prove the intermediate claim HqR: q ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R q HqQ).

We prove the intermediate claim HpP0: p ∈ P0.

An exact proof term for the current goal is (binintersectI rational_numbers I p HpQ HpI).

We prove the intermediate claim HqP0: q ∈ P0.

An exact proof term for the current goal is (binintersectI rational_numbers I q HqQ HqI).

We prove the intermediate claim HpP: p ∈ P.

An exact proof term for the current goal is (binunionI1 P0 (UPair a b) p HpP0).

We prove the intermediate claim HqP: q ∈ P.

An exact proof term for the current goal is (binunionI1 P0 (UPair a b) q HqP0).

Set np to be the term ordsucc (code p).

Set nq to be the term ordsucc (code q).

We prove the intermediate claim HcodepO: code p ∈ ω.

An exact proof term for the current goal is (Hcode_in_omega p HpP).

We prove the intermediate claim HcodeqO: code q ∈ ω.

An exact proof term for the current goal is (Hcode_in_omega q HqP).

We prove the intermediate claim HnpNat: nat_p np.

An exact proof term for the current goal is (omega_nat_p np (omega_ordsucc (code p) HcodepO)).

We prove the intermediate claim HnqNat: nat_p nq.

An exact proof term for the current goal is (omega_nat_p nq (omega_ordsucc (code q) HcodeqO)).

Set n to be the term add_nat np nq.

We prove the intermediate claim HnNat: nat_p n.

An exact proof term for the current goal is (add_nat_p np HnpNat nq HnqNat).

We prove the intermediate claim HpDomNp: p ∈ Fof np.

An exact proof term for the current goal is (Hp_in_dom_succ_code p HpP).

We prove the intermediate claim HqDomNq: q ∈ Fof nq.

An exact proof term for the current goal is (Hp_in_dom_succ_code q HqP).

We prove the intermediate claim HpDomN: p ∈ Fof n.

An exact proof term for the current goal is (Fof_increase_by_add np nq p HnpNat HnqNat HpDomNp).

We prove the intermediate claim HnCom: add_nat np nq = add_nat nq np.

An exact proof term for the current goal is (add_nat_com np HnpNat nq HnqNat).

We prove the intermediate claim HqDomN': q ∈ Fof (add_nat nq np).

An exact proof term for the current goal is (Fof_increase_by_add nq np q HnqNat HnpNat HqDomNq).

We prove the intermediate claim HqDomN: q ∈ Fof n.

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

An exact proof term for the current goal is HqDomN'.

We prove the intermediate claim Hpi: ¬ (Rlt p a) ∧ ¬ (Rlt b p).

An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ¬ (Rlt x0 a) ∧ ¬ (Rlt b x0)) p HpI).

We prove the intermediate claim Hnpa: ¬ (Rlt p a).

An exact proof term for the current goal is (andEL (¬ (Rlt p a)) (¬ (Rlt b p)) Hpi).

We prove the intermediate claim Hnbp: ¬ (Rlt b p).

An exact proof term for the current goal is (andER (¬ (Rlt p a)) (¬ (Rlt b p)) Hpi).

We prove the intermediate claim Hqi: ¬ (Rlt q a) ∧ ¬ (Rlt b q).

An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ¬ (Rlt x0 a) ∧ ¬ (Rlt b x0)) q HqI).

We prove the intermediate claim Hnqa: ¬ (Rlt q a).

An exact proof term for the current goal is (andEL (¬ (Rlt q a)) (¬ (Rlt b q)) Hqi).

We prove the intermediate claim Hnbq: ¬ (Rlt b q).

An exact proof term for the current goal is (andER (¬ (Rlt q a)) (¬ (Rlt b q)) Hqi).

We prove the intermediate claim HUQp: U_Q p = apply_fun (Gof np) p.

We prove the intermediate claim Hbeta: U_Q p = if (Rlt p a) then Empty else (if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p).

Use reflexivity.

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

We prove the intermediate claim Hstep1: (if (Rlt p a) then Empty else (if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p)) = (if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p).

An exact proof term for the current goal is (If_i_0 (Rlt p a) Empty (if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p) Hnpa).

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

We prove the intermediate claim Hstep2: (if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p) = apply_fun (Gof (ordsucc (code p))) p.

An exact proof term for the current goal is (If_i_0 (Rlt b p) X (apply_fun (Gof (ordsucc (code p))) p) Hnbp).

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

Use reflexivity.

We prove the intermediate claim HUQq: U_Q q = apply_fun (Gof nq) q.

We prove the intermediate claim Hbeta: U_Q q = if (Rlt q a) then Empty else (if (Rlt b q) then X else apply_fun (Gof (ordsucc (code q))) q).

Use reflexivity.

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

We prove the intermediate claim Hstep1: (if (Rlt q a) then Empty else (if (Rlt b q) then X else apply_fun (Gof (ordsucc (code q))) q)) = (if (Rlt b q) then X else apply_fun (Gof (ordsucc (code q))) q).

An exact proof term for the current goal is (If_i_0 (Rlt q a) Empty (if (Rlt b q) then X else apply_fun (Gof (ordsucc (code q))) q) Hnqa).

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

We prove the intermediate claim Hstep2: (if (Rlt b q) then X else apply_fun (Gof (ordsucc (code q))) q) = apply_fun (Gof (ordsucc (code q))) q.

An exact proof term for the current goal is (If_i_0 (Rlt b q) X (apply_fun (Gof (ordsucc (code q))) q) Hnbq).

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

Use reflexivity.

We prove the intermediate claim Hpn: apply_fun (Gof n) p = apply_fun (Gof np) p.

An exact proof term for the current goal is (Gof_preserve_add np nq p HnpNat HnqNat HpDomNp).

We prove the intermediate claim Hqn': apply_fun (Gof (add_nat nq np)) q = apply_fun (Gof nq) q.

An exact proof term for the current goal is (Gof_preserve_add nq np q HnqNat HnpNat HqDomNq).

We prove the intermediate claim Hqn: apply_fun (Gof n) q = apply_fun (Gof nq) q.

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

An exact proof term for the current goal is Hqn'.

We prove the intermediate claim Hnest: closure_of X Tx (apply_fun (Gof n) p) ⊆ apply_fun (Gof n) q.

An exact proof term for the current goal is (Inv_nesting_at n p q HnNat HpDomN HqDomN Hpq).

Let x be given.

Assume Hx: x ∈ closure_of X Tx (U_Q p).

We will prove x ∈ U_Q q.

We prove the intermediate claim HUQpN: U_Q p = apply_fun (Gof n) p.

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

Use symmetry.

An exact proof term for the current goal is Hpn.

We prove the intermediate claim HUQqN: U_Q q = apply_fun (Gof n) q.

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

Use symmetry.

An exact proof term for the current goal is Hqn.

We prove the intermediate claim Hx': x ∈ closure_of X Tx (apply_fun (Gof n) p).

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

An exact proof term for the current goal is Hx.

We prove the intermediate claim HxIn: x ∈ apply_fun (Gof n) q.

An exact proof term for the current goal is (Hnest x Hx').

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

An exact proof term for the current goal is HxIn.

We prove the intermediate claim HU_Q_open: ∀p : set, p ∈ rational_numbers → U_Q p ∈ Tx.

Let p be given.

Assume HpQ: p ∈ rational_numbers.

We prove the intermediate claim HpR: p ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R p HpQ).

Apply (xm (Rlt p a)) to the current goal.

Assume Hpa: Rlt p a.

We prove the intermediate claim Hbeta: U_Q p = if (Rlt p a) then Empty else (if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p).

Use reflexivity.

We prove the intermediate claim HU: U_Q p = Empty.

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

An exact proof term for the current goal is (If_i_1 (Rlt p a) Empty (if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p) Hpa).

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

An exact proof term for the current goal is (topology_has_empty X Tx HTx).

Assume Hnpa: ¬ (Rlt p a).

Apply (xm (Rlt b p)) to the current goal.

Assume Hbp: Rlt b p.

We prove the intermediate claim Hbeta: U_Q p = if (Rlt p a) then Empty else (if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p).

Use reflexivity.

We prove the intermediate claim HU: U_Q p = X.

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

We prove the intermediate claim Hstep: (if (Rlt p a) then Empty else (if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p)) = (if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p).

An exact proof term for the current goal is (If_i_0 (Rlt p a) Empty (if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p) Hnpa).

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

An exact proof term for the current goal is (If_i_1 (Rlt b p) X (apply_fun (Gof (ordsucc (code p))) p) Hbp).

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

An exact proof term for the current goal is (topology_has_X X Tx HTx).

Assume Hnbp: ¬ (Rlt b p).

We prove the intermediate claim HpI: p ∈ I.

An exact proof term for the current goal is (SepI R (λx0 : set ⇒ ¬ (Rlt x0 a) ∧ ¬ (Rlt b x0)) p HpR (andI (¬ (Rlt p a)) (¬ (Rlt b p)) Hnpa Hnbp)).

We prove the intermediate claim HpP0: p ∈ P0.

An exact proof term for the current goal is (binintersectI rational_numbers I p HpQ HpI).

We prove the intermediate claim HpP: p ∈ P.

An exact proof term for the current goal is (binunionI1 P0 (UPair a b) p HpP0).

We prove the intermediate claim HpDom: p ∈ Fof (ordsucc (code p)).

An exact proof term for the current goal is (Hp_in_dom_succ_code p HpP).

We prove the intermediate claim HcodepO: code p ∈ ω.

An exact proof term for the current goal is (Hcode_in_omega p HpP).

We prove the intermediate claim HstageNat: nat_p (ordsucc (code p)).

An exact proof term for the current goal is (omega_nat_p (ordsucc (code p)) (omega_ordsucc (code p) HcodepO)).

We prove the intermediate claim HInvStage: Inv (State (ordsucc (code p))).

An exact proof term for the current goal is (HInvAll (ordsucc (code p)) HstageNat).

We prove the intermediate claim HtotState: total_function_on ((State (ordsucc (code p))) 1) ((State (ordsucc (code p))) 0) Tx.

Apply (and6E (finite ((State (ordsucc (code p))) 0)) (((State (ordsucc (code p))) 0 ⊆ R)) (total_function_on ((State (ordsucc (code p))) 1) ((State (ordsucc (code p))) 0) Tx) (functional_graph ((State (ordsucc (code p))) 1)) (graph_domain_subset ((State (ordsucc (code p))) 1) ((State (ordsucc (code p))) 0)) (∀p0 q0 : set, p0 ∈ ((State (ordsucc (code p))) 0) → q0 ∈ ((State (ordsucc (code p))) 0) → Rlt p0 q0 → closure_of X Tx (apply_fun ((State (ordsucc (code p))) 1) p0) ⊆ apply_fun ((State (ordsucc (code p))) 1) q0) HInvStage (total_function_on ((State (ordsucc (code p))) 1) ((State (ordsucc (code p))) 0) Tx)) to the current goal.

Assume Hfin Hsub Htot Hfg Hgd Hnest.

An exact proof term for the current goal is Htot.

We prove the intermediate claim Htot: total_function_on (Gof (ordsucc (code p))) (Fof (ordsucc (code p))) Tx.

We prove the intermediate claim HGofDef: Gof (ordsucc (code p)) = (State (ordsucc (code p))) 1.

Use reflexivity.

We prove the intermediate claim HFofDef: Fof (ordsucc (code p)) = (State (ordsucc (code p))) 0.

Use reflexivity.

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

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

An exact proof term for the current goal is HtotState.

We prove the intermediate claim Hbeta: U_Q p = if (Rlt p a) then Empty else if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p.

Use reflexivity.

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

We prove the intermediate claim Hif1: (if (Rlt p a) then Empty else if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p) = (if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p).

An exact proof term for the current goal is (If_i_0 (Rlt p a) Empty (if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p) Hnpa).

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

We prove the intermediate claim Hif2: (if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p) = apply_fun (Gof (ordsucc (code p))) p.

An exact proof term for the current goal is (If_i_0 (Rlt b p) X (apply_fun (Gof (ordsucc (code p))) p) Hnbp).

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

An exact proof term for the current goal is (total_function_on_apply_fun_in_Y (Gof (ordsucc (code p))) (Fof (ordsucc (code p))) Tx p Htot HpDom).

We prove the intermediate claim HfxRlub: ∀x : set, x ∈ X → R_lub (LB x) (fx x).

Let x be given.

Assume HxX: x ∈ X.

We prove the intermediate claim HLB_nonempty: ∃l0 : set, l0 ∈ LB x.

We use a to witness the existential quantifier.

We prove the intermediate claim HLBdef: LB x = {l ∈ R|∀p : set, p ∈ Qx x → p ∈ R → Rle l p}.

Use reflexivity.

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

We prove the intermediate claim Hprop: ∀p : set, p ∈ Qx x → p ∈ R → Rle a p.

Let p be given.

Assume HpQx: p ∈ Qx x.

Assume HpR: p ∈ R.

We prove the intermediate claim HQxDef: Qx x = {p ∈ rational_numbers|x ∈ U_Q p}.

Use reflexivity.

We prove the intermediate claim HpQx': p ∈ {p ∈ rational_numbers|x ∈ U_Q p}.

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

An exact proof term for the current goal is HpQx.

We prove the intermediate claim HxUp: x ∈ U_Q p.

An exact proof term for the current goal is (SepE2 rational_numbers (λp0 : set ⇒ x ∈ U_Q p0) p HpQx').

Apply (xm (Rlt p a)) to the current goal.

Assume Hpa: Rlt p a.

We prove the intermediate claim HUeq: U_Q p = if (Rlt p a) then Empty else if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p.

Use reflexivity.

We prove the intermediate claim HUempty: U_Q p = Empty.

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

An exact proof term for the current goal is (If_i_1 (Rlt p a) Empty (if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p) Hpa).

We prove the intermediate claim HxEmpty: x ∈ Empty.

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

An exact proof term for the current goal is HxUp.

An exact proof term for the current goal is (FalseE (EmptyE x HxEmpty) (Rle a p)).

Assume Hnpa: ¬ (Rlt p a).

An exact proof term for the current goal is (RleI a p HaR HpR Hnpa).

An exact proof term for the current goal is (SepI R (λl : set ⇒ ∀p : set, p ∈ Qx x → p ∈ R → Rle l p) a HaR Hprop).

We prove the intermediate claim HLB_in_R: ∀l : set, l ∈ LB x → l ∈ R.

Let l be given.

Assume Hl: l ∈ LB x.

An exact proof term for the current goal is (SepE1 R (λl0 : set ⇒ ∀p : set, p ∈ Qx x → p ∈ R → Rle l0 p) l Hl).

We prove the intermediate claim HbS: SNo b.

An exact proof term for the current goal is (real_SNo b HbR).

Set bp1 to be the term add_SNo b 1.

We prove the intermediate claim Hbp1R: bp1 ∈ R.

An exact proof term for the current goal is (real_add_SNo b HbR 1 real_1).

We prove the intermediate claim Hbinpm: b ∈ open_interval (add_SNo b (minus_SNo 1)) (add_SNo b 1).

An exact proof term for the current goal is (real_in_open_interval_minus1_plus1 b HbR).

We prove the intermediate claim HbinpmProp: Rlt (add_SNo b (minus_SNo 1)) b ∧ Rlt b bp1.

An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt (add_SNo b (minus_SNo 1)) z ∧ Rlt z (add_SNo b 1)) b Hbinpm).

We prove the intermediate claim Hb_lt_bp1: Rlt b bp1.

An exact proof term for the current goal is (andER (Rlt (add_SNo b (minus_SNo 1)) b) (Rlt b bp1) HbinpmProp).

Apply (rational_dense_between_reals b bp1 HbR Hbp1R Hb_lt_bp1) to the current goal.

Let q0 be given.

Assume Hq0pair.

Apply Hq0pair to the current goal.

Assume Hq0Q: q0 ∈ rational_numbers.

Assume Hq0Prop: Rlt b q0 ∧ Rlt q0 bp1.

We prove the intermediate claim Hq0R: q0 ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R q0 Hq0Q).

We prove the intermediate claim Hbq0: Rlt b q0.

An exact proof term for the current goal is (andEL (Rlt b q0) (Rlt q0 bp1) Hq0Prop).

We prove the intermediate claim Hq0InQx: q0 ∈ Qx x.

We prove the intermediate claim HQxDef: Qx x = {p ∈ rational_numbers|x ∈ U_Q p}.

Use reflexivity.

We prove the intermediate claim Hq0Sep: q0 ∈ {p ∈ rational_numbers|x ∈ U_Q p}.

We prove the intermediate claim HxU: x ∈ U_Q q0.

We prove the intermediate claim HUeq: U_Q q0 = if (Rlt q0 a) then Empty else if (Rlt b q0) then X else apply_fun (Gof (ordsucc (code q0))) q0.

Use reflexivity.

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

Apply (xm (Rlt q0 a)) to the current goal.

Assume Hqa: Rlt q0 a.

We prove the intermediate claim HifEmpty: (if (Rlt q0 a) then Empty else if (Rlt b q0) then X else apply_fun (Gof (ordsucc (code q0))) q0) = Empty.

An exact proof term for the current goal is (If_i_1 (Rlt q0 a) Empty (if (Rlt b q0) then X else apply_fun (Gof (ordsucc (code q0))) q0) Hqa).

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

We prove the intermediate claim Hba: Rlt b a.

An exact proof term for the current goal is (Rlt_tra b q0 a Hbq0 Hqa).

An exact proof term for the current goal is (FalseE ((RleE_nlt a b Hab) Hba) (x ∈ Empty)).

Assume Hnqa: ¬ (Rlt q0 a).

We prove the intermediate claim HifStep: (if (Rlt q0 a) then Empty else if (Rlt b q0) then X else apply_fun (Gof (ordsucc (code q0))) q0) = (if (Rlt b q0) then X else apply_fun (Gof (ordsucc (code q0))) q0).

An exact proof term for the current goal is (If_i_0 (Rlt q0 a) Empty (if (Rlt b q0) then X else apply_fun (Gof (ordsucc (code q0))) q0) Hnqa).

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

We prove the intermediate claim HifX: (if (Rlt b q0) then X else apply_fun (Gof (ordsucc (code q0))) q0) = X.

An exact proof term for the current goal is (If_i_1 (Rlt b q0) X (apply_fun (Gof (ordsucc (code q0))) q0) Hbq0).

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

An exact proof term for the current goal is HxX.

An exact proof term for the current goal is (SepI rational_numbers (λp0 : set ⇒ x ∈ U_Q p0) q0 Hq0Q HxU).

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

An exact proof term for the current goal is Hq0Sep.

We prove the intermediate claim HLB_upper: ∃u : set, u ∈ R ∧ ∀l : set, l ∈ LB x → l ∈ R → Rle l u.

We use q0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hq0R.

Let l be given.

Assume HlLB: l ∈ LB x.

Assume HlR: l ∈ R.

We prove the intermediate claim Hlprop: ∀p : set, p ∈ Qx x → p ∈ R → Rle l p.

An exact proof term for the current goal is (SepE2 R (λl0 : set ⇒ ∀p : set, p ∈ Qx x → p ∈ R → Rle l0 p) l HlLB).

An exact proof term for the current goal is (Hlprop q0 Hq0InQx Hq0R).

We prove the intermediate claim Hexlub: ∃r : set, R_lub (LB x) r.

An exact proof term for the current goal is (R_lub_exists (LB x) HLB_nonempty HLB_in_R HLB_upper).

An exact proof term for the current goal is (Eps_i_ex (λr : set ⇒ R_lub (LB x) r) Hexlub).

We prove the intermediate claim Hfx_in_R: ∀x : set, x ∈ X → fx x ∈ R.

Let x be given.

Assume HxX: x ∈ X.

An exact proof term for the current goal is (R_lub_in_R (LB x) (fx x) (HfxRlub x HxX)).

We prove the intermediate claim HfunXR: function_on f X R.

Let x be given.

Assume HxX: x ∈ X.

rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ fx x0) x HxX) (from left to right).

An exact proof term for the current goal is (Hfx_in_R x HxX).

We prove the intermediate claim HcontR: continuous_map X Tx R R_standard_topology f.

Set S to be the term open_rays_subbasis R.

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.

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

Apply (continuous_map_from_subbasis X Tx R S f HTx HfunXR HS) to the current goal.

Let s be given.

Assume HsS: s ∈ S.

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 X f 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 X f s ∈ Tx)) to the current goal.

Assume Hsup: s ∈ {I ∈ 𝒫 R|∃a0 ∈ R, I = open_ray_upper R a0}.

We prove the intermediate claim Hexa0: ∃a0 ∈ R, s = open_ray_upper R a0.

An exact proof term for the current goal is (SepE2 (𝒫 R) (λI : set ⇒ ∃a0 ∈ R, I = open_ray_upper R a0) s Hsup).

Apply Hexa0 to the current goal.

Let a0 be given.

Assume Ha0pair.

We prove the intermediate claim Ha0R: a0 ∈ R.

An exact proof term for the current goal is (andEL (a0 ∈ R) (s = open_ray_upper R a0) Ha0pair).

We prove the intermediate claim Hseq: s = open_ray_upper R a0.

An exact proof term for the current goal is (andER (a0 ∈ R) (s = open_ray_upper R a0) Ha0pair).

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

Set Qgt to be the term {q ∈ rational_numbers|Rlt a0 q}.

Set Fam to be the term {X ∖ closure_of X Tx (U_Q q)|q ∈ Qgt}.

We prove the intermediate claim HFamPow: Fam ∈ 𝒫 Tx.

Apply PowerI to the current goal.

Let U be given.

Assume HU: U ∈ Fam.

Apply (ReplE_impred Qgt (λq : set ⇒ X ∖ closure_of X Tx (U_Q q)) U HU (U ∈ Tx)) to the current goal.

Let q be given.

Assume HqQgt: q ∈ Qgt.

Assume HUeq: U = X ∖ closure_of X Tx (U_Q q).

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

We prove the intermediate claim HqQ: q ∈ rational_numbers.

An exact proof term for the current goal is (SepE1 rational_numbers (λq0 : set ⇒ Rlt a0 q0) q HqQgt).

We prove the intermediate claim HUopen: U_Q q ∈ Tx.

An exact proof term for the current goal is (HU_Q_open q HqQ).

We prove the intermediate claim HUsubX: U_Q q ⊆ X.

An exact proof term for the current goal is (topology_elem_subset X Tx (U_Q q) HTx HUopen).

We prove the intermediate claim HclClosed: closed_in X Tx (closure_of X Tx (U_Q q)).

An exact proof term for the current goal is (closure_is_closed X Tx (U_Q q) HTx HUsubX).

An exact proof term for the current goal is (open_in_elem X Tx (X ∖ closure_of X Tx (U_Q q)) (open_of_closed_complement X Tx (closure_of X Tx (U_Q q)) HclClosed)).

We prove the intermediate claim HpreEq: preimage_of X f (open_ray_upper R a0) = ⋃ Fam.

Apply set_ext to the current goal.

Let x be given.

Assume Hx: x ∈ preimage_of X f (open_ray_upper R a0).

We will prove x ∈ ⋃ Fam.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (SepE1 X (λu : set ⇒ apply_fun f u ∈ open_ray_upper R a0) x Hx).

We prove the intermediate claim HfxIn: apply_fun f x ∈ open_ray_upper R a0.

An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun f u ∈ open_ray_upper R a0) x Hx).

We prove the intermediate claim HfxR: apply_fun f x ∈ R.

An exact proof term for the current goal is (HfunXR x HxX).

We prove the intermediate claim HltRel: order_rel R a0 (apply_fun f x).

An exact proof term for the current goal is (SepE2 R (λy : set ⇒ order_rel R a0 y) (apply_fun f x) HfxIn).

We prove the intermediate claim Hlt: Rlt a0 (apply_fun f x).

An exact proof term for the current goal is (order_rel_R_implies_Rlt a0 (apply_fun f x) HltRel).

Apply (rational_dense_between_reals a0 (apply_fun f x) Ha0R HfxR Hlt) to the current goal.

Let q be given.

Assume Hqpair.

Apply Hqpair to the current goal.

Assume HqQ: q ∈ rational_numbers.

Assume HqProp: Rlt a0 q ∧ Rlt q (apply_fun f x).

We prove the intermediate claim Ha0q: Rlt a0 q.

An exact proof term for the current goal is (andEL (Rlt a0 q) (Rlt q (apply_fun f x)) HqProp).

We prove the intermediate claim Hqltfx: Rlt q (apply_fun f x).

An exact proof term for the current goal is (andER (Rlt a0 q) (Rlt q (apply_fun f x)) HqProp).

We prove the intermediate claim HqInQgt: q ∈ Qgt.

An exact proof term for the current goal is (SepI rational_numbers (λq0 : set ⇒ Rlt a0 q0) q HqQ Ha0q).

We prove the intermediate claim HclNot: x ∈ (X ∖ closure_of X Tx (U_Q q)).

We prove the intermediate claim Hnotcl: x ∉ closure_of X Tx (U_Q q).

Assume Hxcl: x ∈ closure_of X Tx (U_Q q).

We prove the intermediate claim Hfxlub: R_lub (LB x) (fx x).

An exact proof term for the current goal is (HfxRlub x HxX).

We prove the intermediate claim HfxEq: apply_fun f x = fx x.

We prove the intermediate claim HfDef: f = graph X (λx0 : set ⇒ fx x0).

Use reflexivity.

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

An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ fx x0) x HxX).

We prove the intermediate claim Hqltfx_fx: Rlt q (fx x).

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

An exact proof term for the current goal is Hqltfx.

We prove the intermediate claim Hcore: (fx x ∈ R ∧ ∀l : set, l ∈ LB x → l ∈ R → Rle l (fx x)).

An exact proof term for the current goal is (andEL (fx x ∈ R ∧ ∀l : set, l ∈ LB x → l ∈ R → Rle l (fx x)) (∀u : set, u ∈ R → (∀l : set, l ∈ LB x → l ∈ R → Rle l u) → Rle (fx x) u) Hfxlub).

We prove the intermediate claim HfxR: fx x ∈ R.

An exact proof term for the current goal is (andEL (fx x ∈ R) (∀l : set, l ∈ LB x → l ∈ R → Rle l (fx x)) Hcore).

We prove the intermediate claim HminLB: ∀u : set, u ∈ R → (∀l : set, l ∈ LB x → l ∈ R → Rle l u) → Rle (fx x) u.

An exact proof term for the current goal is (andER (fx x ∈ R ∧ ∀l : set, l ∈ LB x → l ∈ R → Rle l (fx x)) (∀u : set, u ∈ R → (∀l : set, l ∈ LB x → l ∈ R → Rle l u) → Rle (fx x) u) Hfxlub).

We prove the intermediate claim HqR: q ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R q HqQ).

We prove the intermediate claim HLB_le_b: ∀l : set, l ∈ LB x → l ∈ R → Rle l b.

Let l be given.

Assume HlLB: l ∈ LB x.

Assume HlR: l ∈ R.

Apply (xm (Rlt b l)) to the current goal.

Assume Hbl: Rlt b l.

Apply (rational_dense_between_reals b l HbR HlR Hbl) to the current goal.

Let p be given.

Assume HpPair.

Apply HpPair to the current goal.

Assume HpQ: p ∈ rational_numbers.

Assume HpProp: Rlt b p ∧ Rlt p l.

We prove the intermediate claim Hbp: Rlt b p.

An exact proof term for the current goal is (andEL (Rlt b p) (Rlt p l) HpProp).

We prove the intermediate claim Hpl: Rlt p l.

An exact proof term for the current goal is (andER (Rlt b p) (Rlt p l) HpProp).

We prove the intermediate claim HpR: p ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R p HpQ).

We prove the intermediate claim Hnpa: ¬ (Rlt p a).

Assume Hpa: Rlt p a.

We prove the intermediate claim Hpb: Rlt p b.

An exact proof term for the current goal is (Rlt_Rle_tra p a b Hpa Hab).

We prove the intermediate claim Hbb: Rlt b b.

An exact proof term for the current goal is (Rlt_tra b p b Hbp Hpb).

An exact proof term for the current goal is (not_Rlt_refl b HbR Hbb).

We prove the intermediate claim HUeq: U_Q p = if (Rlt p a) then Empty else if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p.

Use reflexivity.

We prove the intermediate claim Hstep: (if (Rlt p a) then Empty else if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p) = (if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p).

An exact proof term for the current goal is (If_i_0 (Rlt p a) Empty (if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p) Hnpa).

We prove the intermediate claim HUX: U_Q p = X.

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

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

An exact proof term for the current goal is (If_i_1 (Rlt b p) X (apply_fun (Gof (ordsucc (code p))) p) Hbp).

We prove the intermediate claim HxUp: x ∈ U_Q p.

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

An exact proof term for the current goal is HxX.

We prove the intermediate claim HpQx: p ∈ Qx x.

An exact proof term for the current goal is (SepI rational_numbers (λp0 : set ⇒ x ∈ U_Q p0) p HpQ HxUp).

We prove the intermediate claim HlProp: ∀p0 : set, p0 ∈ Qx x → p0 ∈ R → Rle l p0.

An exact proof term for the current goal is (SepE2 R (λl0 : set ⇒ ∀p0 : set, p0 ∈ Qx x → p0 ∈ R → Rle l0 p0) l HlLB).

We prove the intermediate claim Hlelp: Rle l p.

An exact proof term for the current goal is (HlProp p HpQx HpR).

We prove the intermediate claim Hcontra: False.

An exact proof term for the current goal is ((RleE_nlt l p Hlelp) Hpl).

An exact proof term for the current goal is (FalseE Hcontra (Rle l b)).

Assume Hnbl: ¬ (Rlt b l).

An exact proof term for the current goal is (RleI l b HlR HbR Hnbl).

We prove the intermediate claim Hfxleb: Rle (fx x) b.

An exact proof term for the current goal is (HminLB b HbR HLB_le_b).

We prove the intermediate claim Hqltb: Rlt q b.

An exact proof term for the current goal is (Rlt_Rle_tra q (fx x) b Hqltfx_fx Hfxleb).

We prove the intermediate claim Hnbq: ¬ (Rlt b q).

Assume Hbq': Rlt b q.

We prove the intermediate claim Hbb: Rlt b b.

An exact proof term for the current goal is (Rlt_tra b q b Hbq' Hqltb).

An exact proof term for the current goal is (not_Rlt_refl b HbR Hbb).

We prove the intermediate claim Hnqa: ¬ (Rlt q a).

Apply (xm (Rlt q a)) to the current goal.

Assume Hqa: Rlt q a.

We prove the intermediate claim HUeq: U_Q q = if (Rlt q a) then Empty else if (Rlt b q) then X else apply_fun (Gof (ordsucc (code q))) q.

Use reflexivity.

We prove the intermediate claim HUempty: U_Q q = Empty.

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

An exact proof term for the current goal is (If_i_1 (Rlt q a) Empty (if (Rlt b q) then X else apply_fun (Gof (ordsucc (code q))) q) Hqa).

We prove the intermediate claim Hclq: closure_of X Tx (U_Q q) = Empty.

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

An exact proof term for the current goal is (closure_of_empty X Tx HTx).

We prove the intermediate claim HxE: x ∈ Empty.

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

An exact proof term for the current goal is Hxcl.

An exact proof term for the current goal is (FalseE (EmptyE x HxE) (¬ (Rlt q a))).

Assume Hnqa': ¬ (Rlt q a).

An exact proof term for the current goal is Hnqa'.

We prove the intermediate claim HqI: q ∈ I.

An exact proof term for the current goal is (SepI R (λx0 : set ⇒ ¬ (Rlt x0 a) ∧ ¬ (Rlt b x0)) q HqR (andI (¬ (Rlt q a)) (¬ (Rlt b q)) Hnqa Hnbq)).

We prove the intermediate claim Hub_q: ∀l : set, l ∈ LB x → l ∈ R → Rle l q.

Let l be given.

Assume HlLB: l ∈ LB x.

Assume HlR: l ∈ R.

Apply (xm (Rlt q l)) to the current goal.

Assume Hql: Rlt q l.

We prove the intermediate claim Hleb: Rle l b.

An exact proof term for the current goal is (HLB_le_b l HlLB HlR).

Apply (rational_dense_between_reals q l HqR HlR Hql) to the current goal.

Let r be given.

Assume HrPair.

Apply HrPair to the current goal.

Assume HrQ: r ∈ rational_numbers.

Assume HrProp: Rlt q r ∧ Rlt r l.

We prove the intermediate claim Hqr: Rlt q r.

An exact proof term for the current goal is (andEL (Rlt q r) (Rlt r l) HrProp).

We prove the intermediate claim Hrl: Rlt r l.

An exact proof term for the current goal is (andER (Rlt q r) (Rlt r l) HrProp).

We prove the intermediate claim HrR: r ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R r HrQ).

We prove the intermediate claim Hrlb: Rlt r b.

An exact proof term for the current goal is (Rlt_Rle_tra r l b Hrl Hleb).

We prove the intermediate claim Hnbr: ¬ (Rlt b r).

Assume Hbr: Rlt b r.

We prove the intermediate claim Hbb: Rlt b b.

An exact proof term for the current goal is (Rlt_tra b r b Hbr Hrlb).

An exact proof term for the current goal is (not_Rlt_refl b HbR Hbb).

We prove the intermediate claim Hnra: ¬ (Rlt r a).

Assume Hra: Rlt r a.

We prove the intermediate claim Hqa: Rlt q a.

An exact proof term for the current goal is (Rlt_tra q r a Hqr Hra).

An exact proof term for the current goal is (Hnqa Hqa).

We prove the intermediate claim HrI: r ∈ I.

An exact proof term for the current goal is (SepI R (λx0 : set ⇒ ¬ (Rlt x0 a) ∧ ¬ (Rlt b x0)) r HrR (andI (¬ (Rlt r a)) (¬ (Rlt b r)) Hnra Hnbr)).

We prove the intermediate claim HclSub: closure_of X Tx (U_Q q) ⊆ U_Q r.

An exact proof term for the current goal is (U_Q_closure_mono_I q r HqQ HrQ HqI HrI Hqr).

We prove the intermediate claim HxUr: x ∈ U_Q r.

An exact proof term for the current goal is (HclSub x Hxcl).

We prove the intermediate claim HrQx: r ∈ Qx x.

An exact proof term for the current goal is (SepI rational_numbers (λp0 : set ⇒ x ∈ U_Q p0) r HrQ HxUr).

We prove the intermediate claim HlProp: ∀p0 : set, p0 ∈ Qx x → p0 ∈ R → Rle l p0.

An exact proof term for the current goal is (SepE2 R (λl0 : set ⇒ ∀p0 : set, p0 ∈ Qx x → p0 ∈ R → Rle l0 p0) l HlLB).

We prove the intermediate claim Hlelr: Rle l r.

An exact proof term for the current goal is (HlProp r HrQx HrR).

We prove the intermediate claim Hcontra: False.

An exact proof term for the current goal is ((RleE_nlt l r Hlelr) Hrl).

An exact proof term for the current goal is (FalseE Hcontra (Rle l q)).

Assume Hnql: ¬ (Rlt q l).

An exact proof term for the current goal is (RleI l q HlR HqR Hnql).

We prove the intermediate claim Hfxleq: Rle (fx x) q.

An exact proof term for the current goal is (HminLB q HqR Hub_q).

An exact proof term for the current goal is ((RleE_nlt (fx x) q Hfxleq) Hqltfx_fx).

An exact proof term for the current goal is (setminusI X (closure_of X Tx (U_Q q)) x HxX Hnotcl).

We prove the intermediate claim HFam: (X ∖ closure_of X Tx (U_Q q)) ∈ Fam.

An exact proof term for the current goal is (ReplI Qgt (λq0 : set ⇒ X ∖ closure_of X Tx (U_Q q0)) q HqInQgt).

An exact proof term for the current goal is (UnionI Fam x (X ∖ closure_of X Tx (U_Q q)) HclNot HFam).

Let x be given.

Assume Hx: x ∈ ⋃ Fam.

We will prove x ∈ preimage_of X f (open_ray_upper R a0).

Apply (UnionE_impred Fam x Hx) to the current goal.

Let U be given.

Assume HxU: x ∈ U.

Assume HUin: U ∈ Fam.

Apply (ReplE_impred Qgt (λq : set ⇒ X ∖ closure_of X Tx (U_Q q)) U HUin (x ∈ preimage_of X f (open_ray_upper R a0))) to the current goal.

Let q be given.

Assume HqIn: q ∈ Qgt.

Assume HUeq: U = X ∖ closure_of X Tx (U_Q q).

We prove the intermediate claim HxUdiff: x ∈ X ∖ closure_of X Tx (U_Q q).

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

An exact proof term for the current goal is HxU.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (setminusE1 X (closure_of X Tx (U_Q q)) x HxUdiff).

We prove the intermediate claim HxNotCl: x ∉ closure_of X Tx (U_Q q).

An exact proof term for the current goal is (setminusE2 X (closure_of X Tx (U_Q q)) x HxUdiff).

We prove the intermediate claim HqQ: q ∈ rational_numbers.

An exact proof term for the current goal is (SepE1 rational_numbers (λq0 : set ⇒ Rlt a0 q0) q HqIn).

We prove the intermediate claim Ha0q: Rlt a0 q.

An exact proof term for the current goal is (SepE2 rational_numbers (λq0 : set ⇒ Rlt a0 q0) q HqIn).

We prove the intermediate claim HqR: q ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R q HqQ).

We prove the intermediate claim HfxEq: apply_fun f x = fx x.

We prove the intermediate claim HfDef: f = graph X (λx0 : set ⇒ fx x0).

Use reflexivity.

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

An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ fx x0) x HxX).

We prove the intermediate claim Hfxlub: R_lub (LB x) (fx x).

An exact proof term for the current goal is (HfxRlub x HxX).

We prove the intermediate claim HQx_no_small: ∀p0 : set, p0 ∈ Qx x → p0 ∈ R → Rle q p0.

Let p0 be given.

Assume Hp0Qx: p0 ∈ Qx x.

Assume Hp0R: p0 ∈ R.

Apply (xm (Rlt p0 q)) to the current goal.

Assume Hp0lt: Rlt p0 q.

Apply FalseE to the current goal.

We prove the intermediate claim Hp0Q: p0 ∈ rational_numbers.

An exact proof term for the current goal is (SepE1 rational_numbers (λp1 : set ⇒ x ∈ U_Q p1) p0 Hp0Qx).

We prove the intermediate claim HxUp0: x ∈ U_Q p0.

An exact proof term for the current goal is (SepE2 rational_numbers (λp1 : set ⇒ x ∈ U_Q p1) p0 Hp0Qx).

We prove the intermediate claim HqQ': q ∈ rational_numbers.

An exact proof term for the current goal is HqQ.

We prove the intermediate claim HqR': q ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R q HqQ').

We prove the intermediate claim Hnqa: ¬ (Rlt q a).

Assume Hqa: Rlt q a.

We prove the intermediate claim Hp0a: Rlt p0 a.

An exact proof term for the current goal is (Rlt_tra p0 q a Hp0lt Hqa).

We prove the intermediate claim HUeq: U_Q p0 = if (Rlt p0 a) then Empty else if (Rlt b p0) then X else apply_fun (Gof (ordsucc (code p0))) p0.

Use reflexivity.

We prove the intermediate claim HUempty: U_Q p0 = Empty.

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

An exact proof term for the current goal is (If_i_1 (Rlt p0 a) Empty (if (Rlt b p0) then X else apply_fun (Gof (ordsucc (code p0))) p0) Hp0a).

We prove the intermediate claim HxE: x ∈ Empty.

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

An exact proof term for the current goal is HxUp0.

An exact proof term for the current goal is (EmptyE x HxE).

We prove the intermediate claim Hnbq: ¬ (Rlt b q).

Assume Hbq: Rlt b q.

We prove the intermediate claim HUeq: U_Q q = if (Rlt q a) then Empty else if (Rlt b q) then X else apply_fun (Gof (ordsucc (code q))) q.

Use reflexivity.

We prove the intermediate claim Hnq1: (if (Rlt q a) then Empty else if (Rlt b q) then X else apply_fun (Gof (ordsucc (code q))) q) = (if (Rlt b q) then X else apply_fun (Gof (ordsucc (code q))) q).

An exact proof term for the current goal is (If_i_0 (Rlt q a) Empty (if (Rlt b q) then X else apply_fun (Gof (ordsucc (code q))) q) Hnqa).

We prove the intermediate claim HUX: U_Q q = X.

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

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

An exact proof term for the current goal is (If_i_1 (Rlt b q) X (apply_fun (Gof (ordsucc (code q))) q) Hbq).

We prove the intermediate claim Hclq: closure_of X Tx (U_Q q) = X.

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

An exact proof term for the current goal is (closure_of_space X Tx HTx).

We prove the intermediate claim Hxcl: x ∈ closure_of X Tx (U_Q q).

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

An exact proof term for the current goal is HxX.

An exact proof term for the current goal is (HxNotCl Hxcl).

We prove the intermediate claim HqI: q ∈ I.

An exact proof term for the current goal is (SepI R (λx0 : set ⇒ ¬ (Rlt x0 a) ∧ ¬ (Rlt b x0)) q HqR' (andI (¬ (Rlt q a)) (¬ (Rlt b q)) Hnqa Hnbq)).

We prove the intermediate claim Hp0R': p0 ∈ R.

An exact proof term for the current goal is Hp0R.

We prove the intermediate claim Hnp0a: ¬ (Rlt p0 a).

Assume Hp0a: Rlt p0 a.

We prove the intermediate claim HUeq: U_Q p0 = if (Rlt p0 a) then Empty else if (Rlt b p0) then X else apply_fun (Gof (ordsucc (code p0))) p0.

Use reflexivity.

We prove the intermediate claim HUempty: U_Q p0 = Empty.

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

An exact proof term for the current goal is (If_i_1 (Rlt p0 a) Empty (if (Rlt b p0) then X else apply_fun (Gof (ordsucc (code p0))) p0) Hp0a).

We prove the intermediate claim HxE: x ∈ Empty.

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

An exact proof term for the current goal is HxUp0.

An exact proof term for the current goal is (EmptyE x HxE).

We prove the intermediate claim Hnbp0: ¬ (Rlt b p0).

Assume Hbp0: Rlt b p0.

We prove the intermediate claim Hbq: Rlt b q.

An exact proof term for the current goal is (Rlt_tra b p0 q Hbp0 Hp0lt).

An exact proof term for the current goal is (Hnbq Hbq).

We prove the intermediate claim Hp0I: p0 ∈ I.

An exact proof term for the current goal is (SepI R (λx0 : set ⇒ ¬ (Rlt x0 a) ∧ ¬ (Rlt b x0)) p0 Hp0R' (andI (¬ (Rlt p0 a)) (¬ (Rlt b p0)) Hnp0a Hnbp0)).

We prove the intermediate claim HclSub: closure_of X Tx (U_Q p0) ⊆ U_Q q.

An exact proof term for the current goal is (U_Q_closure_mono_I p0 q Hp0Q HqQ' Hp0I HqI Hp0lt).

We prove the intermediate claim HUopen: U_Q p0 ∈ Tx.

An exact proof term for the current goal is (HU_Q_open p0 Hp0Q).

We prove the intermediate claim HUsubX: U_Q p0 ⊆ X.

An exact proof term for the current goal is (topology_elem_subset X Tx (U_Q p0) HTx HUopen).

We prove the intermediate claim Hsubcl: U_Q p0 ⊆ closure_of X Tx (U_Q p0).

An exact proof term for the current goal is (subset_of_closure X Tx (U_Q p0) HTx HUsubX).

We prove the intermediate claim Hxclp0: x ∈ closure_of X Tx (U_Q p0).

An exact proof term for the current goal is (Hsubcl x HxUp0).

We prove the intermediate claim HxUq: x ∈ U_Q q.

An exact proof term for the current goal is (HclSub x Hxclp0).

We prove the intermediate claim HUqOpen: U_Q q ∈ Tx.

An exact proof term for the current goal is (HU_Q_open q HqQ').

We prove the intermediate claim HUqSubX: U_Q q ⊆ X.

An exact proof term for the current goal is (topology_elem_subset X Tx (U_Q q) HTx HUqOpen).

We prove the intermediate claim Hxclq: x ∈ closure_of X Tx (U_Q q).

An exact proof term for the current goal is ((subset_of_closure X Tx (U_Q q) HTx HUqSubX) x HxUq).

An exact proof term for the current goal is (HxNotCl Hxclq).

Assume Hnlt: ¬ (Rlt p0 q).

An exact proof term for the current goal is (RleI q p0 HqR Hp0R Hnlt).

We prove the intermediate claim HqInLB: q ∈ LB x.

An exact proof term for the current goal is (SepI R (λl : set ⇒ ∀p0 : set, p0 ∈ Qx x → p0 ∈ R → Rle l p0) q HqR HQx_no_small).

We prove the intermediate claim Hub: Rle q (fx x).

An exact proof term for the current goal is (andER (fx x ∈ R) (∀a1 : set, a1 ∈ LB x → a1 ∈ R → Rle a1 (fx x)) (andEL (fx x ∈ R ∧ (∀a1 : set, a1 ∈ LB x → a1 ∈ R → Rle a1 (fx x))) (∀u : set, u ∈ R → (∀a1 : set, a1 ∈ LB x → a1 ∈ R → Rle a1 u) → Rle (fx x) u) Hfxlub) q HqInLB HqR).

We prove the intermediate claim Ha0fx: Rlt a0 (fx x).

An exact proof term for the current goal is (Rlt_Rle_tra a0 q (fx x) Ha0q Hub).

We prove the intermediate claim Ha0fxrel: order_rel R a0 (apply_fun f x).

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

An exact proof term for the current goal is (Rlt_implies_order_rel_R a0 (fx x) Ha0fx).

We prove the intermediate claim HfxIn: apply_fun f x ∈ open_ray_upper R a0.

An exact proof term for the current goal is (SepI R (λy : set ⇒ order_rel R a0 y) (apply_fun f x) (HfunXR x HxX) Ha0fxrel).

An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun f u ∈ open_ray_upper R a0) x HxX HfxIn).

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

An exact proof term for the current goal is (topology_union_closed_pow X Tx Fam HTx HFamPow).

Assume Hslo: s ∈ {I ∈ 𝒫 R|∃b0 ∈ R, I = open_ray_lower R b0}.

We prove the intermediate claim Hexb0: ∃b0 ∈ R, s = open_ray_lower R b0.

An exact proof term for the current goal is (SepE2 (𝒫 R) (λI : set ⇒ ∃b0 ∈ R, I = open_ray_lower R b0) s Hslo).

Apply Hexb0 to the current goal.

Let b0 be given.

Assume Hb0pair.

We prove the intermediate claim Hb0R: b0 ∈ R.

An exact proof term for the current goal is (andEL (b0 ∈ R) (s = open_ray_lower R b0) Hb0pair).

We prove the intermediate claim Hseq: s = open_ray_lower R b0.

An exact proof term for the current goal is (andER (b0 ∈ R) (s = open_ray_lower R b0) Hb0pair).

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

Set Qlt to be the term {q ∈ rational_numbers|Rlt q b0}.

Set FamL to be the term {U_Q q|q ∈ Qlt}.

We prove the intermediate claim HFamPow: FamL ∈ 𝒫 Tx.

Apply PowerI to the current goal.

Let U be given.

Assume HU: U ∈ FamL.

Apply (ReplE_impred Qlt (λq : set ⇒ U_Q q) U HU (U ∈ Tx)) to the current goal.

Let q be given.

Assume HqQlt: q ∈ Qlt.

Assume HUeq: U = U_Q q.

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

We prove the intermediate claim HqQ: q ∈ rational_numbers.

An exact proof term for the current goal is (SepE1 rational_numbers (λq0 : set ⇒ Rlt q0 b0) q HqQlt).

An exact proof term for the current goal is (HU_Q_open q HqQ).

We prove the intermediate claim HpreEq: preimage_of X f (open_ray_lower R b0) = ⋃ FamL.

Apply set_ext to the current goal.

Let x be given.

Assume Hx: x ∈ preimage_of X f (open_ray_lower R b0).

We will prove x ∈ ⋃ FamL.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (SepE1 X (λu : set ⇒ apply_fun f u ∈ open_ray_lower R b0) x Hx).

We prove the intermediate claim HfxIn: apply_fun f x ∈ open_ray_lower R b0.

An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun f u ∈ open_ray_lower R b0) x Hx).

We prove the intermediate claim HfxR: apply_fun f x ∈ R.

An exact proof term for the current goal is (HfunXR x HxX).

We prove the intermediate claim HltRel: order_rel R (apply_fun f x) b0.

An exact proof term for the current goal is (SepE2 R (λy : set ⇒ order_rel R y b0) (apply_fun f x) HfxIn).

We prove the intermediate claim Hlt: Rlt (apply_fun f x) b0.

An exact proof term for the current goal is (order_rel_R_implies_Rlt (apply_fun f x) b0 HltRel).

Apply (rational_dense_between_reals (apply_fun f x) b0 HfxR Hb0R Hlt) to the current goal.

Let q be given.

Assume Hqpair.

Apply Hqpair to the current goal.

Assume HqQ: q ∈ rational_numbers.

Assume HqProp: Rlt (apply_fun f x) q ∧ Rlt q b0.

We prove the intermediate claim Hfxltq: Rlt (apply_fun f x) q.

An exact proof term for the current goal is (andEL (Rlt (apply_fun f x) q) (Rlt q b0) HqProp).

We prove the intermediate claim Hqltb0: Rlt q b0.

An exact proof term for the current goal is (andER (Rlt (apply_fun f x) q) (Rlt q b0) HqProp).

We prove the intermediate claim HfxEq: apply_fun f x = fx x.

We prove the intermediate claim HfDef: f = graph X (λx0 : set ⇒ fx x0).

Use reflexivity.

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

An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ fx x0) x HxX).

We prove the intermediate claim Hfxlub: R_lub (LB x) (fx x).

An exact proof term for the current goal is (HfxRlub x HxX).

We prove the intermediate claim Hcore: (fx x ∈ R ∧ ∀l : set, l ∈ LB x → l ∈ R → Rle l (fx x)).

We prove the intermediate claim HfxR': fx x ∈ R.

An exact proof term for the current goal is (andEL (fx x ∈ R) (∀l : set, l ∈ LB x → l ∈ R → Rle l (fx x)) Hcore).

We prove the intermediate claim HubLB: ∀l : set, l ∈ LB x → l ∈ R → Rle l (fx x).

An exact proof term for the current goal is (andER (fx x ∈ R) (∀l : set, l ∈ LB x → l ∈ R → Rle l (fx x)) Hcore).

We prove the intermediate claim HminLB: ∀u : set, u ∈ R → (∀l : set, l ∈ LB x → l ∈ R → Rle l u) → Rle (fx x) u.

We prove the intermediate claim Hqltfx: Rlt (fx x) q.

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

An exact proof term for the current goal is Hfxltq.

We prove the intermediate claim HqR: q ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R q HqQ).

We prove the intermediate claim HnotLB: q ∉ LB x.

Assume HqLB: q ∈ LB x.

We prove the intermediate claim Hle: Rle q (fx x).

An exact proof term for the current goal is (HubLB q HqLB HqR).

An exact proof term for the current goal is ((RleE_nlt q (fx x) Hle) Hqltfx).

We prove the intermediate claim HnotForall: ¬ (∀p0 : set, p0 ∈ Qx x → p0 ∈ R → Rle q p0).

Assume Hall: ∀p0 : set, p0 ∈ Qx x → p0 ∈ R → Rle q p0.

We prove the intermediate claim HqLB: q ∈ LB x.

An exact proof term for the current goal is (SepI R (λl : set ⇒ ∀p0 : set, p0 ∈ Qx x → p0 ∈ R → Rle l p0) q HqR Hall).

An exact proof term for the current goal is (HnotLB HqLB).

Apply (not_all_ex_demorgan_i (λp0 : set ⇒ p0 ∈ Qx x → p0 ∈ R → Rle q p0) HnotForall) to the current goal.

Let p0 be given.

Assume Hnp0.

We prove the intermediate claim Hnp0imp: ¬ (p0 ∈ Qx x → p0 ∈ R → Rle q p0).

An exact proof term for the current goal is Hnp0.

Apply (not_imp (p0 ∈ Qx x) (p0 ∈ R → Rle q p0) Hnp0imp) to the current goal.

Assume Hp0Qx: p0 ∈ Qx x.

Assume Hnimp2: ¬ (p0 ∈ R → Rle q p0).

Apply (not_imp (p0 ∈ R) (Rle q p0) Hnimp2) to the current goal.

Assume Hp0R: p0 ∈ R.

Assume Hnle: ¬ (Rle q p0).

Apply (xm (Rlt p0 q)) to the current goal.

Assume Hp0ltq: Rlt p0 q.

We prove the intermediate claim Hp0Q: p0 ∈ rational_numbers.

An exact proof term for the current goal is (SepE1 rational_numbers (λp1 : set ⇒ x ∈ U_Q p1) p0 Hp0Qx).

We prove the intermediate claim HxUp0: x ∈ U_Q p0.

An exact proof term for the current goal is (SepE2 rational_numbers (λp1 : set ⇒ x ∈ U_Q p1) p0 Hp0Qx).

Apply (xm (Rlt b q)) to the current goal.

Assume Hbq: Rlt b q.

We prove the intermediate claim Hnqa: ¬ (Rlt q a).

Assume Hqa: Rlt q a.

We prove the intermediate claim Hba: Rlt b a.

An exact proof term for the current goal is (Rlt_tra b q a Hbq Hqa).

An exact proof term for the current goal is ((RleE_nlt a b Hab) Hba).

We prove the intermediate claim HUeq: U_Q q = if (Rlt q a) then Empty else if (Rlt b q) then X else apply_fun (Gof (ordsucc (code q))) q.

Use reflexivity.

We prove the intermediate claim HUqX: U_Q q = X.

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

We prove the intermediate claim Hstep: (if (Rlt q a) then Empty else if (Rlt b q) then X else apply_fun (Gof (ordsucc (code q))) q) = (if (Rlt b q) then X else apply_fun (Gof (ordsucc (code q))) q).

An exact proof term for the current goal is (If_i_0 (Rlt q a) Empty (if (Rlt b q) then X else apply_fun (Gof (ordsucc (code q))) q) Hnqa).

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

An exact proof term for the current goal is (If_i_1 (Rlt b q) X (apply_fun (Gof (ordsucc (code q))) q) Hbq).

We prove the intermediate claim HxUq: x ∈ U_Q q.

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

An exact proof term for the current goal is HxX.

We prove the intermediate claim HqInQlt: q ∈ Qlt.

An exact proof term for the current goal is (SepI rational_numbers (λq0 : set ⇒ Rlt q0 b0) q HqQ Hqltb0).

We prove the intermediate claim HqFam: U_Q q ∈ FamL.

An exact proof term for the current goal is (ReplI Qlt (λq0 : set ⇒ U_Q q0) q HqInQlt).

An exact proof term for the current goal is (UnionI FamL x (U_Q q) HxUq HqFam).

Assume Hnbq: ¬ (Rlt b q).

We prove the intermediate claim Hnqa: ¬ (Rlt q a).

Assume Hqa: Rlt q a.

We prove the intermediate claim Hp0a: Rlt p0 a.

An exact proof term for the current goal is (Rlt_tra p0 q a Hp0ltq Hqa).

We prove the intermediate claim HUeq: U_Q p0 = if (Rlt p0 a) then Empty else if (Rlt b p0) then X else apply_fun (Gof (ordsucc (code p0))) p0.

Use reflexivity.

We prove the intermediate claim HUempty: U_Q p0 = Empty.

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

An exact proof term for the current goal is (If_i_1 (Rlt p0 a) Empty (if (Rlt b p0) then X else apply_fun (Gof (ordsucc (code p0))) p0) Hp0a).

We prove the intermediate claim HxE: x ∈ Empty.

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

An exact proof term for the current goal is HxUp0.

An exact proof term for the current goal is (EmptyE x HxE).

We prove the intermediate claim HqI: q ∈ I.

An exact proof term for the current goal is (SepI R (λx0 : set ⇒ ¬ (Rlt x0 a) ∧ ¬ (Rlt b x0)) q HqR (andI (¬ (Rlt q a)) (¬ (Rlt b q)) Hnqa Hnbq)).

We prove the intermediate claim Hp0I: p0 ∈ I.

We prove the intermediate claim Hnp0a: ¬ (Rlt p0 a).

Assume Hp0a: Rlt p0 a.

We prove the intermediate claim HUeq: U_Q p0 = if (Rlt p0 a) then Empty else if (Rlt b p0) then X else apply_fun (Gof (ordsucc (code p0))) p0.

Use reflexivity.

We prove the intermediate claim HUempty: U_Q p0 = Empty.

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

An exact proof term for the current goal is (If_i_1 (Rlt p0 a) Empty (if (Rlt b p0) then X else apply_fun (Gof (ordsucc (code p0))) p0) Hp0a).

We prove the intermediate claim HxE: x ∈ Empty.

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

An exact proof term for the current goal is HxUp0.

An exact proof term for the current goal is (EmptyE x HxE).

We prove the intermediate claim Hnbp0: ¬ (Rlt b p0).

Assume Hbp0: Rlt b p0.

We prove the intermediate claim Hbq': Rlt b q.

An exact proof term for the current goal is (Rlt_tra b p0 q Hbp0 Hp0ltq).

An exact proof term for the current goal is (Hnbq Hbq').

An exact proof term for the current goal is (SepI R (λx0 : set ⇒ ¬ (Rlt x0 a) ∧ ¬ (Rlt b x0)) p0 Hp0R (andI (¬ (Rlt p0 a)) (¬ (Rlt b p0)) Hnp0a Hnbp0)).

We prove the intermediate claim HclSub: closure_of X Tx (U_Q p0) ⊆ U_Q q.

An exact proof term for the current goal is (U_Q_closure_mono_I p0 q Hp0Q HqQ Hp0I HqI Hp0ltq).

We prove the intermediate claim HUopen: U_Q p0 ∈ Tx.

An exact proof term for the current goal is (HU_Q_open p0 Hp0Q).

We prove the intermediate claim HUsubX: U_Q p0 ⊆ X.

An exact proof term for the current goal is (topology_elem_subset X Tx (U_Q p0) HTx HUopen).

We prove the intermediate claim Hxclp0: x ∈ closure_of X Tx (U_Q p0).

An exact proof term for the current goal is ((subset_of_closure X Tx (U_Q p0) HTx HUsubX) x HxUp0).

We prove the intermediate claim HxUq: x ∈ U_Q q.

An exact proof term for the current goal is (HclSub x Hxclp0).

We prove the intermediate claim HqInQlt: q ∈ Qlt.

An exact proof term for the current goal is (SepI rational_numbers (λq0 : set ⇒ Rlt q0 b0) q HqQ Hqltb0).

We prove the intermediate claim HqFam: U_Q q ∈ FamL.

An exact proof term for the current goal is (ReplI Qlt (λq0 : set ⇒ U_Q q0) q HqInQlt).

An exact proof term for the current goal is (UnionI FamL x (U_Q q) HxUq HqFam).

Assume Hnlt: ¬ (Rlt p0 q).

We prove the intermediate claim Hle: Rle q p0.

An exact proof term for the current goal is (RleI q p0 HqR Hp0R Hnlt).

An exact proof term for the current goal is (FalseE (Hnle Hle) (x ∈ ⋃ FamL)).

Let x be given.

Assume Hx: x ∈ ⋃ FamL.

We will prove x ∈ preimage_of X f (open_ray_lower R b0).

Apply (UnionE_impred FamL x Hx) to the current goal.

Let U be given.

Assume HxU: x ∈ U.

Assume HUin: U ∈ FamL.

Apply (ReplE_impred Qlt (λq : set ⇒ U_Q q) U HUin (x ∈ preimage_of X f (open_ray_lower R b0))) to the current goal.

Let q be given.

Assume HqIn: q ∈ Qlt.

Assume HUeq: U = U_Q q.

We prove the intermediate claim HqQ: q ∈ rational_numbers.

An exact proof term for the current goal is (SepE1 rational_numbers (λq0 : set ⇒ Rlt q0 b0) q HqIn).

We prove the intermediate claim Hqltb0: Rlt q b0.

An exact proof term for the current goal is (SepE2 rational_numbers (λq0 : set ⇒ Rlt q0 b0) q HqIn).

We prove the intermediate claim HqR: q ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R q HqQ).

We prove the intermediate claim HxUq: x ∈ U_Q q.

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

An exact proof term for the current goal is HxU.

We prove the intermediate claim HxX: x ∈ X.

We prove the intermediate claim HUopen: U_Q q ∈ Tx.

An exact proof term for the current goal is (HU_Q_open q HqQ).

An exact proof term for the current goal is (topology_elem_subset X Tx (U_Q q) HTx HUopen x HxUq).

We prove the intermediate claim HfxEq: apply_fun f x = fx x.

We prove the intermediate claim HfDef: f = graph X (λx0 : set ⇒ fx x0).

Use reflexivity.

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

An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ fx x0) x HxX).

We prove the intermediate claim Hfxlub: R_lub (LB x) (fx x).

An exact proof term for the current goal is (HfxRlub x HxX).

We prove the intermediate claim HminLB: ∀u : set, u ∈ R → (∀l : set, l ∈ LB x → l ∈ R → Rle l u) → Rle (fx x) u.

We prove the intermediate claim HqUpper: ∀l : set, l ∈ LB x → l ∈ R → Rle l q.

Let l be given.

Assume HlLB: l ∈ LB x.

Assume HlR: l ∈ R.

We prove the intermediate claim HlProp: ∀p0 : set, p0 ∈ Qx x → p0 ∈ R → Rle l p0.

An exact proof term for the current goal is (SepE2 R (λl0 : set ⇒ ∀p0 : set, p0 ∈ Qx x → p0 ∈ R → Rle l0 p0) l HlLB).

We prove the intermediate claim HqQx: q ∈ Qx x.

An exact proof term for the current goal is (SepI rational_numbers (λp0 : set ⇒ x ∈ U_Q p0) q HqQ HxUq).

An exact proof term for the current goal is (HlProp q HqQx HqR).

We prove the intermediate claim Hfxleq: Rle (fx x) q.

An exact proof term for the current goal is (HminLB q HqR HqUpper).

We prove the intermediate claim Hfxltb0: Rlt (apply_fun f x) b0.

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

An exact proof term for the current goal is (Rle_Rlt_tra (fx x) q b0 Hfxleq Hqltb0).

We prove the intermediate claim HfxRel: order_rel R (apply_fun f x) b0.

An exact proof term for the current goal is (Rlt_implies_order_rel_R (apply_fun f x) b0 Hfxltb0).

An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun f u ∈ open_ray_lower R b0) x HxX (SepI R (λy : set ⇒ order_rel R y b0) (apply_fun f x) (HfunXR x HxX) HfxRel)).

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

An exact proof term for the current goal is (topology_union_closed_pow X Tx FamL HTx HFamPow).

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).

We prove the intermediate claim HpreWhole: preimage_of X f R = X.

An exact proof term for the current goal is (preimage_of_whole X R f HfunXR).

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

An exact proof term for the current goal is (topology_has_X X Tx HTx).

An exact proof term for the current goal is HsS.

We prove the intermediate claim HimgI: ∀x : set, x ∈ X → apply_fun f x ∈ I.

Let x be given.

Assume HxX: x ∈ X.

We prove the intermediate claim HfxEq: apply_fun f x = fx x.

We prove the intermediate claim HfDef: f = graph X (λx0 : set ⇒ fx x0).

Use reflexivity.

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

An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ fx x0) x HxX).

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

We prove the intermediate claim Hfxlub: R_lub (LB x) (fx x).

An exact proof term for the current goal is (HfxRlub x HxX).

We prove the intermediate claim Hcore: (fx x ∈ R ∧ ∀l : set, l ∈ LB x → l ∈ R → Rle l (fx x)).

We prove the intermediate claim HubLB: ∀l : set, l ∈ LB x → l ∈ R → Rle l (fx x).

An exact proof term for the current goal is (andER (fx x ∈ R) (∀l : set, l ∈ LB x → l ∈ R → Rle l (fx x)) Hcore).

We prove the intermediate claim HminLB: ∀u : set, u ∈ R → (∀l : set, l ∈ LB x → l ∈ R → Rle l u) → Rle (fx x) u.

We prove the intermediate claim HaLB: a ∈ LB x.

We prove the intermediate claim Hprop: ∀p : set, p ∈ Qx x → p ∈ R → Rle a p.

Let p be given.

Assume HpQx: p ∈ Qx x.

Assume HpR: p ∈ R.

We prove the intermediate claim HQxDef: Qx x = {p0 ∈ rational_numbers|x ∈ U_Q p0}.

Use reflexivity.

We prove the intermediate claim HpSep: p ∈ {p0 ∈ rational_numbers|x ∈ U_Q p0}.

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

An exact proof term for the current goal is HpQx.

We prove the intermediate claim HxUp: x ∈ U_Q p.

An exact proof term for the current goal is (SepE2 rational_numbers (λp0 : set ⇒ x ∈ U_Q p0) p HpSep).

Apply (xm (Rlt p a)) to the current goal.

Assume Hpa: Rlt p a.

We prove the intermediate claim HUeq: U_Q p = if (Rlt p a) then Empty else if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p.

Use reflexivity.

We prove the intermediate claim HUempty: U_Q p = Empty.

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

An exact proof term for the current goal is (If_i_1 (Rlt p a) Empty (if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p) Hpa).

We prove the intermediate claim HxEmpty: x ∈ Empty.

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

An exact proof term for the current goal is HxUp.

An exact proof term for the current goal is (FalseE (EmptyE x HxEmpty) (Rle a p)).

Assume Hnpa: ¬ (Rlt p a).

An exact proof term for the current goal is (RleI a p HaR HpR Hnpa).

An exact proof term for the current goal is (SepI R (λl : set ⇒ ∀p : set, p ∈ Qx x → p ∈ R → Rle l p) a HaR Hprop).

We prove the intermediate claim Hale: Rle a (fx x).

An exact proof term for the current goal is (HubLB a HaLB HaR).

We prove the intermediate claim HLB_le_b: ∀l : set, l ∈ LB x → l ∈ R → Rle l b.

Let l be given.

Assume HlLB: l ∈ LB x.

Assume HlR: l ∈ R.

Apply (xm (Rlt b l)) to the current goal.

Assume Hbl: Rlt b l.

Apply (rational_dense_between_reals b l HbR HlR Hbl) to the current goal.

Let p be given.

Assume HpPair.

Apply HpPair to the current goal.

Assume HpQ: p ∈ rational_numbers.

Assume HpProp: Rlt b p ∧ Rlt p l.

We prove the intermediate claim Hbp: Rlt b p.

An exact proof term for the current goal is (andEL (Rlt b p) (Rlt p l) HpProp).

We prove the intermediate claim Hpl: Rlt p l.

An exact proof term for the current goal is (andER (Rlt b p) (Rlt p l) HpProp).

We prove the intermediate claim HpR: p ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R p HpQ).

We prove the intermediate claim HUeq: U_Q p = if (Rlt p a) then Empty else if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p.

Use reflexivity.

We prove the intermediate claim Hnpa: ¬ (Rlt p a).

Assume Hpa: Rlt p a.

We prove the intermediate claim Hpb: Rlt p b.

An exact proof term for the current goal is (Rlt_Rle_tra p a b Hpa Hab).

We prove the intermediate claim Hbb: Rlt b b.

An exact proof term for the current goal is (Rlt_tra b p b Hbp Hpb).

An exact proof term for the current goal is (not_Rlt_refl b HbR Hbb).

We prove the intermediate claim Hstep: (if (Rlt p a) then Empty else if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p) = (if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p).

An exact proof term for the current goal is (If_i_0 (Rlt p a) Empty (if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p) Hnpa).

We prove the intermediate claim HUX: U_Q p = X.

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

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

An exact proof term for the current goal is (If_i_1 (Rlt b p) X (apply_fun (Gof (ordsucc (code p))) p) Hbp).

We prove the intermediate claim HxUp: x ∈ U_Q p.

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

An exact proof term for the current goal is HxX.

We prove the intermediate claim HQxDef: Qx x = {p0 ∈ rational_numbers|x ∈ U_Q p0}.

Use reflexivity.

We prove the intermediate claim HpQx: p ∈ Qx x.

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

An exact proof term for the current goal is (SepI rational_numbers (λp0 : set ⇒ x ∈ U_Q p0) p HpQ HxUp).

We prove the intermediate claim HlProp: ∀p0 : set, p0 ∈ Qx x → p0 ∈ R → Rle l p0.

An exact proof term for the current goal is (SepE2 R (λl0 : set ⇒ ∀p0 : set, p0 ∈ Qx x → p0 ∈ R → Rle l0 p0) l HlLB).

We prove the intermediate claim Hlelp: Rle l p.

An exact proof term for the current goal is (HlProp p HpQx HpR).

We prove the intermediate claim Hcontra: False.

An exact proof term for the current goal is ((RleE_nlt l p Hlelp) Hpl).

An exact proof term for the current goal is (FalseE Hcontra (Rle l b)).

Assume Hnbl: ¬ (Rlt b l).

An exact proof term for the current goal is (RleI l b HlR HbR Hnbl).

We prove the intermediate claim Hleb: Rle (fx x) b.

An exact proof term for the current goal is (HminLB b HbR HLB_le_b).

We prove the intermediate claim Hnfxa: ¬ (Rlt (fx x) a).

An exact proof term for the current goal is (RleE_nlt a (fx x) Hale).

We prove the intermediate claim Hnbfx: ¬ (Rlt b (fx x)).

An exact proof term for the current goal is (RleE_nlt (fx x) b Hleb).

An exact proof term for the current goal is (SepI R (λr : set ⇒ ¬ (Rlt r a) ∧ ¬ (Rlt b r)) (fx x) (Hfx_in_R x HxX) (andI (¬ (Rlt (fx x) a)) (¬ (Rlt b (fx x))) Hnfxa Hnbfx)).

We prove the intermediate claim HcontI: continuous_map X Tx I Ti f.

An exact proof term for the current goal is (continuous_map_range_restrict X Tx R R_standard_topology f I HcontR HISubR HimgI).

We use f to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HcontI.

Let x be given.

Assume HxA: x ∈ A.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (HAsubX x HxA).

We prove the intermediate claim HfxEq: apply_fun f x = fx x.

We prove the intermediate claim HfDef: f = graph X (λx0 : set ⇒ fx x0).

Use reflexivity.

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

An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ fx x0) x HxX).

We prove the intermediate claim HfxR: fx x ∈ R.

An exact proof term for the current goal is (Hfx_in_R x HxX).

We prove the intermediate claim Hfxlub: R_lub (LB x) (fx x).

An exact proof term for the current goal is (HfxRlub x HxX).

We prove the intermediate claim HminLB: ∀u : set, u ∈ R → (∀l : set, l ∈ LB x → l ∈ R → Rle l u) → Rle (fx x) u.

We prove the intermediate claim HfxI: fx x ∈ I.

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

An exact proof term for the current goal is (HimgI x HxX).

We prove the intermediate claim HfxIcore: ¬ (Rlt (fx x) a) ∧ ¬ (Rlt b (fx x)).

An exact proof term for the current goal is (SepE2 R (λr : set ⇒ ¬ (Rlt r a) ∧ ¬ (Rlt b r)) (fx x) HfxI).

We prove the intermediate claim Hnfxa: ¬ (Rlt (fx x) a).

An exact proof term for the current goal is (andEL (¬ (Rlt (fx x) a)) (¬ (Rlt b (fx x))) HfxIcore).

We prove the intermediate claim Hale: Rle a (fx x).

An exact proof term for the current goal is (RleI a (fx x) HaR HfxR Hnfxa).

We prove the intermediate claim HxA_in_UQ_gt_a: ∀q : set, q ∈ rational_numbers → Rlt a q → x ∈ U_Q q.

Let q be given.

Assume HqQ: q ∈ rational_numbers.

Assume Haq: Rlt a q.

We prove the intermediate claim HqR: q ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R q HqQ).

We prove the intermediate claim Hnqa: ¬ (Rlt q a).

An exact proof term for the current goal is (not_Rlt_sym a q Haq).

Apply (xm (Rlt b q)) to the current goal.

Assume Hbq: Rlt b q.

We prove the intermediate claim HUeq: U_Q q = if (Rlt q a) then Empty else if (Rlt b q) then X else apply_fun (Gof (ordsucc (code q))) q.

Use reflexivity.

We prove the intermediate claim Hstep: (if (Rlt q a) then Empty else if (Rlt b q) then X else apply_fun (Gof (ordsucc (code q))) q) = (if (Rlt b q) then X else apply_fun (Gof (ordsucc (code q))) q).

An exact proof term for the current goal is (If_i_0 (Rlt q a) Empty (if (Rlt b q) then X else apply_fun (Gof (ordsucc (code q))) q) Hnqa).

We prove the intermediate claim HUX: U_Q q = X.

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

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

An exact proof term for the current goal is (If_i_1 (Rlt b q) X (apply_fun (Gof (ordsucc (code q))) q) Hbq).

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

An exact proof term for the current goal is HxX.

Assume Hnbq: ¬ (Rlt b q).

We prove the intermediate claim HqI: q ∈ I.

An exact proof term for the current goal is (SepI R (λr : set ⇒ ¬ (Rlt r a) ∧ ¬ (Rlt b r)) q HqR (andI (¬ (Rlt q a)) (¬ (Rlt b q)) Hnqa Hnbq)).

We prove the intermediate claim HqP0: q ∈ P0.

An exact proof term for the current goal is (binintersectI rational_numbers I q HqQ HqI).

We prove the intermediate claim HqP: q ∈ P.

An exact proof term for the current goal is (binunionI1 P0 (UPair a b) q HqP0).

Set nq to be the term ordsucc (code q).

We prove the intermediate claim HcodeqO: code q ∈ ω.

An exact proof term for the current goal is (Hcode_in_omega q HqP).

We prove the intermediate claim HnqNat: nat_p nq.

An exact proof term for the current goal is (omega_nat_p nq (omega_ordsucc (code q) HcodeqO)).

We prove the intermediate claim HqDom: q ∈ Fof nq.

An exact proof term for the current goal is (Hp_in_dom_succ_code q HqP).

We prove the intermediate claim HSt0: State 0 = BaseState.

An exact proof term for the current goal is (nat_primrec_0 BaseState StepState).

We prove the intermediate claim HFof0: Fof 0 = BaseF.

We prove the intermediate claim HFdef: Fof 0 = (State 0) 0.

Use reflexivity.

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

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

rewrite the current goal using (tuple_2_0_eq BaseF BaseG) (from left to right).

Use reflexivity.

We prove the intermediate claim HaF0: a ∈ Fof 0.

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

An exact proof term for the current goal is (UPairI1 a b).

We prove the intermediate claim HaFq': a ∈ Fof (add_nat 0 nq).

An exact proof term for the current goal is (Fof_increase_by_add 0 nq a nat_0 HnqNat HaF0).

We prove the intermediate claim Hadd0: add_nat 0 nq = nq.

An exact proof term for the current goal is (add_nat_0L nq HnqNat).

We prove the intermediate claim HaDom: a ∈ Fof nq.

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

An exact proof term for the current goal is HaFq'.

We prove the intermediate claim Hnest: closure_of X Tx (apply_fun (Gof nq) a) ⊆ apply_fun (Gof nq) q.

An exact proof term for the current goal is (Inv_nesting_at nq a q HnqNat HaDom HqDom Haq).

We prove the intermediate claim HGof0: Gof 0 = BaseG.

We prove the intermediate claim HGdef: Gof 0 = (State 0) 1.

Use reflexivity.

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

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

rewrite the current goal using (tuple_2_1_eq BaseF BaseG) (from left to right).

Use reflexivity.

We prove the intermediate claim HGa0: apply_fun (Gof 0) a = U_a.

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

An exact proof term for the current goal is HBaseGa.

We prove the intermediate claim HGa: apply_fun (Gof nq) a = U_a.

We prove the intermediate claim Hpres: apply_fun (Gof (add_nat 0 nq)) a = apply_fun (Gof 0) a.

An exact proof term for the current goal is (Gof_preserve_add 0 nq a nat_0 HnqNat HaF0).

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

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

An exact proof term for the current goal is HGa0.

We prove the intermediate claim HUQq: U_Q q = apply_fun (Gof nq) q.

We prove the intermediate claim Hbeta: U_Q q = if (Rlt q a) then Empty else (if (Rlt b q) then X else apply_fun (Gof (ordsucc (code q))) q).

Use reflexivity.

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

An exact proof term for the current goal is (If_i_0 (Rlt q a) Empty (if (Rlt b q) then X else apply_fun (Gof (ordsucc (code q))) q) Hnqa).

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

We prove the intermediate claim Hstep2: (if (Rlt b q) then X else apply_fun (Gof (ordsucc (code q))) q) = apply_fun (Gof (ordsucc (code q))) q.

An exact proof term for the current goal is (If_i_0 (Rlt b q) X (apply_fun (Gof (ordsucc (code q))) q) Hnbq).

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

Use reflexivity.

We prove the intermediate claim HU_a12: U_a ∈ Tx ∧ A ⊆ U_a.

An exact proof term for the current goal is (andEL (U_a ∈ Tx ∧ A ⊆ U_a) (closure_of X Tx U_a ⊆ U_b) HU_a).

We prove the intermediate claim HAsubUa: A ⊆ U_a.

An exact proof term for the current goal is (andER (U_a ∈ Tx) (A ⊆ U_a) HU_a12).

We prove the intermediate claim HxUa: x ∈ U_a.

An exact proof term for the current goal is (HAsubUa x HxA).

We prove the intermediate claim HU_aTx': U_a ∈ Tx.

An exact proof term for the current goal is (andEL (U_a ∈ Tx) (A ⊆ U_a) HU_a12).

We prove the intermediate claim HU_aSubX: U_a ⊆ X.

An exact proof term for the current goal is (topology_elem_subset X Tx U_a HTx HU_aTx').

We prove the intermediate claim HxclUa: x ∈ closure_of X Tx U_a.

An exact proof term for the current goal is ((subset_of_closure X Tx U_a HTx HU_aSubX) x HxUa).

We prove the intermediate claim HclSub: closure_of X Tx U_a ⊆ U_Q q.

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

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

An exact proof term for the current goal is Hnest.

An exact proof term for the current goal is (HclSub x HxclUa).

We prove the intermediate claim HLB_le_a: ∀l : set, l ∈ LB x → l ∈ R → Rle l a.

Let l be given.

Assume HlLB: l ∈ LB x.

Assume HlR: l ∈ R.

Apply (xm (Rlt a l)) to the current goal.

Assume Halt: Rlt a l.

Apply (rational_dense_between_reals a l HaR HlR Halt) to the current goal.

Let q be given.

Assume Hqpair.

Apply Hqpair to the current goal.

Assume HqQ: q ∈ rational_numbers.

Assume HqProp: Rlt a q ∧ Rlt q l.

We prove the intermediate claim Haq: Rlt a q.

An exact proof term for the current goal is (andEL (Rlt a q) (Rlt q l) HqProp).

We prove the intermediate claim Hql: Rlt q l.

An exact proof term for the current goal is (andER (Rlt a q) (Rlt q l) HqProp).

We prove the intermediate claim HqR: q ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R q HqQ).

We prove the intermediate claim HxUq: x ∈ U_Q q.

An exact proof term for the current goal is (HxA_in_UQ_gt_a q HqQ Haq).

We prove the intermediate claim HqQx: q ∈ Qx x.

An exact proof term for the current goal is (SepI rational_numbers (λp0 : set ⇒ x ∈ U_Q p0) q HqQ HxUq).

We prove the intermediate claim HlProp: ∀p0 : set, p0 ∈ Qx x → p0 ∈ R → Rle l p0.

An exact proof term for the current goal is (SepE2 R (λl0 : set ⇒ ∀p0 : set, p0 ∈ Qx x → p0 ∈ R → Rle l0 p0) l HlLB).

We prove the intermediate claim Hle: Rle l q.

An exact proof term for the current goal is (HlProp q HqQx HqR).

We prove the intermediate claim Hcontra: False.

An exact proof term for the current goal is ((RleE_nlt l q Hle) Hql).

An exact proof term for the current goal is (FalseE Hcontra (Rle l a)).

Assume Hnalt: ¬ (Rlt a l).

An exact proof term for the current goal is (RleI l a HlR HaR Hnalt).

We prove the intermediate claim Hfxlea: Rle (fx x) a.

An exact proof term for the current goal is (HminLB a HaR HLB_le_a).

We prove the intermediate claim HfxEqA: fx x = a.

An exact proof term for the current goal is (Rle_antisym (fx x) a Hfxlea Hale).

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

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

Use reflexivity.

Let x be given.

Assume HxB: x ∈ B.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (HBsubX x HxB).

We prove the intermediate claim HfxEq: apply_fun f x = fx x.

We prove the intermediate claim HfDef: f = graph X (λx0 : set ⇒ fx x0).

Use reflexivity.

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

An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ fx x0) x HxX).

We prove the intermediate claim HfxR: fx x ∈ R.

An exact proof term for the current goal is (Hfx_in_R x HxX).

We prove the intermediate claim Hfxlub: R_lub (LB x) (fx x).

An exact proof term for the current goal is (HfxRlub x HxX).

We prove the intermediate claim HubLB: ∀l : set, l ∈ LB x → l ∈ R → Rle l (fx x).

An exact proof term for the current goal is (andER (fx x ∈ R) (∀l : set, l ∈ LB x → l ∈ R → Rle l (fx x)) (andEL (fx x ∈ R ∧ ∀l : set, l ∈ LB x → l ∈ R → Rle l (fx x)) (∀u : set, u ∈ R → (∀l : set, l ∈ LB x → l ∈ R → Rle l u) → Rle (fx x) u) Hfxlub)).

We prove the intermediate claim HminLB: ∀u : set, u ∈ R → (∀l : set, l ∈ LB x → l ∈ R → Rle l u) → Rle (fx x) u.

We prove the intermediate claim HbLB: b ∈ LB x.

We prove the intermediate claim HLBDef: LB x = {l ∈ R|∀p : set, p ∈ Qx x → p ∈ R → Rle l p}.

Use reflexivity.

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

We prove the intermediate claim Hbprop: ∀p : set, p ∈ Qx x → p ∈ R → Rle b p.

Let p be given.

Assume HpQx: p ∈ Qx x.

Assume HpR: p ∈ R.

We prove the intermediate claim HpQ: p ∈ rational_numbers.

An exact proof term for the current goal is (SepE1 rational_numbers (λp0 : set ⇒ x ∈ U_Q p0) p HpQx).

We prove the intermediate claim HxUp: x ∈ U_Q p.

An exact proof term for the current goal is (SepE2 rational_numbers (λp0 : set ⇒ x ∈ U_Q p0) p HpQx).

Apply (xm (Rlt p b)) to the current goal.

Assume Hpb: Rlt p b.

We prove the intermediate claim HnpA: ¬ (Rlt p a).

Assume Hpa: Rlt p a.

We prove the intermediate claim HUeq: U_Q p = if (Rlt p a) then Empty else if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p.

Use reflexivity.

We prove the intermediate claim HUempty: U_Q p = Empty.

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

An exact proof term for the current goal is (If_i_1 (Rlt p a) Empty (if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p) Hpa).

We prove the intermediate claim HxE: x ∈ Empty.

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

An exact proof term for the current goal is HxUp.

An exact proof term for the current goal is (EmptyE x HxE).

We prove the intermediate claim Hnbp: ¬ (Rlt b p).

An exact proof term for the current goal is (not_Rlt_sym p b Hpb).

We prove the intermediate claim HpI: p ∈ I.

An exact proof term for the current goal is (SepI R (λr : set ⇒ ¬ (Rlt r a) ∧ ¬ (Rlt b r)) p HpR (andI (¬ (Rlt p a)) (¬ (Rlt b p)) HnpA Hnbp)).

We prove the intermediate claim HpP0: p ∈ P0.

An exact proof term for the current goal is (binintersectI rational_numbers I p HpQ HpI).

We prove the intermediate claim HpP: p ∈ P.

An exact proof term for the current goal is (binunionI1 P0 (UPair a b) p HpP0).

Set np to be the term ordsucc (code p).

We prove the intermediate claim HcodepO: code p ∈ ω.

An exact proof term for the current goal is (Hcode_in_omega p HpP).

We prove the intermediate claim HnpNat: nat_p np.

An exact proof term for the current goal is (omega_nat_p np (omega_ordsucc (code p) HcodepO)).

We prove the intermediate claim HpDom: p ∈ Fof np.

An exact proof term for the current goal is (Hp_in_dom_succ_code p HpP).

We prove the intermediate claim HSt0: State 0 = BaseState.

An exact proof term for the current goal is (nat_primrec_0 BaseState StepState).

We prove the intermediate claim HFof0: Fof 0 = BaseF.

We prove the intermediate claim HFdef: Fof 0 = (State 0) 0.

Use reflexivity.

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

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

rewrite the current goal using (tuple_2_0_eq BaseF BaseG) (from left to right).

Use reflexivity.

We prove the intermediate claim HbF0: b ∈ Fof 0.

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

An exact proof term for the current goal is (UPairI2 a b).

We prove the intermediate claim HbFp': b ∈ Fof (add_nat 0 np).

An exact proof term for the current goal is (Fof_increase_by_add 0 np b nat_0 HnpNat HbF0).

We prove the intermediate claim Hadd0: add_nat 0 np = np.

An exact proof term for the current goal is (add_nat_0L np HnpNat).

We prove the intermediate claim HbDom: b ∈ Fof np.

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

An exact proof term for the current goal is HbFp'.

We prove the intermediate claim Hnest: closure_of X Tx (apply_fun (Gof np) p) ⊆ apply_fun (Gof np) b.

An exact proof term for the current goal is (Inv_nesting_at np p b HnpNat HpDom HbDom Hpb).

We prove the intermediate claim HUQp: U_Q p = apply_fun (Gof np) p.

We prove the intermediate claim Hbeta: U_Q p = if (Rlt p a) then Empty else (if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p).

Use reflexivity.

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

An exact proof term for the current goal is (If_i_0 (Rlt p a) Empty (if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p) HnpA).

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

We prove the intermediate claim Hstep2: (if (Rlt b p) then X else apply_fun (Gof (ordsucc (code p))) p) = apply_fun (Gof (ordsucc (code p))) p.

An exact proof term for the current goal is (If_i_0 (Rlt b p) X (apply_fun (Gof (ordsucc (code p))) p) Hnbp).

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

Use reflexivity.

We prove the intermediate claim HGof0: Gof 0 = BaseG.

We prove the intermediate claim HGdef: Gof 0 = (State 0) 1.

Use reflexivity.

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

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

rewrite the current goal using (tuple_2_1_eq BaseF BaseG) (from left to right).

Use reflexivity.

We prove the intermediate claim HGb0: apply_fun (Gof 0) b = U_b.

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

An exact proof term for the current goal is HBaseGb.

We prove the intermediate claim HGb: apply_fun (Gof np) b = U_b.

We prove the intermediate claim Hpres: apply_fun (Gof (add_nat 0 np)) b = apply_fun (Gof 0) b.

An exact proof term for the current goal is (Gof_preserve_add 0 np b nat_0 HnpNat HbF0).

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

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

An exact proof term for the current goal is HGb0.

We prove the intermediate claim HclSub: closure_of X Tx (U_Q p) ⊆ U_b.

Let y be given.

Assume Hy: y ∈ closure_of X Tx (U_Q p).

We will prove y ∈ U_b.

We prove the intermediate claim Hy': y ∈ closure_of X Tx (apply_fun (Gof np) p).

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

An exact proof term for the current goal is Hy.

We prove the intermediate claim Hyb: y ∈ apply_fun (Gof np) b.

An exact proof term for the current goal is (Hnest y Hy').

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

An exact proof term for the current goal is Hyb.

We prove the intermediate claim HUopen: U_Q p ∈ Tx.

An exact proof term for the current goal is (HU_Q_open p HpQ).

We prove the intermediate claim HUpSubX: U_Q p ⊆ X.

An exact proof term for the current goal is (topology_elem_subset X Tx (U_Q p) HTx HUopen).

We prove the intermediate claim Hxclp: x ∈ closure_of X Tx (U_Q p).

An exact proof term for the current goal is ((subset_of_closure X Tx (U_Q p) HTx HUpSubX) x HxUp).

We prove the intermediate claim HxUb: x ∈ U_b.

An exact proof term for the current goal is (HclSub x Hxclp).

We prove the intermediate claim HxNotUb: x ∉ U_b.

Assume HxUb': x ∈ U_b.

We prove the intermediate claim HxNotB: x ∉ B.

An exact proof term for the current goal is (setminusE2 X B x HxUb').

An exact proof term for the current goal is (HxNotB HxB).

An exact proof term for the current goal is (FalseE (HxNotUb HxUb) (Rle b p)).

Assume Hnpb: ¬ (Rlt p b).

An exact proof term for the current goal is (RleI b p HbR HpR Hnpb).

An exact proof term for the current goal is (SepI R (λl : set ⇒ ∀p : set, p ∈ Qx x → p ∈ R → Rle l p) b HbR Hbprop).

We prove the intermediate claim Hleb: Rle b (fx x).

An exact proof term for the current goal is (HubLB b HbLB HbR).

We prove the intermediate claim HLB_le_b: ∀l : set, l ∈ LB x → l ∈ R → Rle l b.

Let l be given.

Assume HlLB: l ∈ LB x.

Assume HlR: l ∈ R.

Apply (xm (Rlt b l)) to the current goal.

Assume Hbl: Rlt b l.

Apply (rational_dense_between_reals b l HbR HlR Hbl) to the current goal.

Let q be given.

Assume HqPair.

Apply HqPair to the current goal.

Assume HqQ: q ∈ rational_numbers.

Assume HqProp: Rlt b q ∧ Rlt q l.

We prove the intermediate claim Hbq: Rlt b q.

An exact proof term for the current goal is (andEL (Rlt b q) (Rlt q l) HqProp).

We prove the intermediate claim Hql: Rlt q l.

An exact proof term for the current goal is (andER (Rlt b q) (Rlt q l) HqProp).

We prove the intermediate claim HqR: q ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R q HqQ).

We prove the intermediate claim Hnqa: ¬ (Rlt q a).

Assume Hqa: Rlt q a.

We prove the intermediate claim Hba': Rlt b a.

An exact proof term for the current goal is (Rlt_tra b q a Hbq Hqa).

An exact proof term for the current goal is ((RleE_nlt a b Hab) Hba').

We prove the intermediate claim HUeq: U_Q q = if (Rlt q a) then Empty else if (Rlt b q) then X else apply_fun (Gof (ordsucc (code q))) q.

Use reflexivity.

We prove the intermediate claim Hstep: (if (Rlt q a) then Empty else if (Rlt b q) then X else apply_fun (Gof (ordsucc (code q))) q) = (if (Rlt b q) then X else apply_fun (Gof (ordsucc (code q))) q).

An exact proof term for the current goal is (If_i_0 (Rlt q a) Empty (if (Rlt b q) then X else apply_fun (Gof (ordsucc (code q))) q) Hnqa).

We prove the intermediate claim HUX: U_Q q = X.

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

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

An exact proof term for the current goal is (If_i_1 (Rlt b q) X (apply_fun (Gof (ordsucc (code q))) q) Hbq).

We prove the intermediate claim HxUq: x ∈ U_Q q.

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

An exact proof term for the current goal is HxX.

We prove the intermediate claim HqQx: q ∈ Qx x.

An exact proof term for the current goal is (SepI rational_numbers (λp0 : set ⇒ x ∈ U_Q p0) q HqQ HxUq).

We prove the intermediate claim HlProp: ∀p0 : set, p0 ∈ Qx x → p0 ∈ R → Rle l p0.

An exact proof term for the current goal is (SepE2 R (λl0 : set ⇒ ∀p0 : set, p0 ∈ Qx x → p0 ∈ R → Rle l0 p0) l HlLB).

We prove the intermediate claim Hle: Rle l q.

An exact proof term for the current goal is (HlProp q HqQx HqR).

We prove the intermediate claim Hcontra: False.

An exact proof term for the current goal is ((RleE_nlt l q Hle) Hql).

An exact proof term for the current goal is (FalseE Hcontra (Rle l b)).

Assume Hnbl: ¬ (Rlt b l).

An exact proof term for the current goal is (RleI l b HlR HbR Hnbl).

We prove the intermediate claim Hfxleb: Rle (fx x) b.

An exact proof term for the current goal is (HminLB b HbR HLB_le_b).

We prove the intermediate claim HfxEqB: fx x = b.

An exact proof term for the current goal is (Rle_antisym (fx x) b Hfxleb Hleb).

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

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

Use reflexivity.