Apply SNoLev_ind to the current goal.

Let x be given.

Assume Hx: SNo x.

Assume IH: ∀w ∈ SNoS_ (SNoLev x), SNoLev w ∈ ω → 0 ≤ w → sqrt_SNo_nonneg w ∈ real.

Assume Hx1: SNoLev x ∈ ω.

Assume Hx2: 0 ≤ x.

We prove the intermediate claim Lx: x ∈ real.

Apply SNoS_omega_real to the current goal.

Apply SNoS_I ω omega_ordinal x (SNoLev x) Hx1 to the current goal.

We will prove SNo_ (SNoLev x) x.

An exact proof term for the current goal is SNoLev_ x Hx.

We will prove sqrt_SNo_nonneg x ∈ real.

Apply ordinal_In_Or_Subq 0 (SNoLev x) ordinal_Empty (SNoLev_ordinal x Hx) to the current goal.

Assume H1: 0 ∈ SNoLev x.

Apply ordinal_In_Or_Subq 1 (SNoLev x) ordinal_1 (SNoLev_ordinal x Hx) to the current goal.

Assume H2: 1 ∈ SNoLev x.

We will prove sqrt_SNo_nonneg x ∈ real.

rewrite the current goal using sqrt_SNo_nonneg_eq x Hx (from left to right).

Set L_ to be the term λk : set ⇒ SNo_sqrtaux x sqrt_SNo_nonneg k 0.

Set R_ to be the term λk : set ⇒ SNo_sqrtaux x sqrt_SNo_nonneg k 1.

Set L to be the term ⋃_{k ∈ ω}L_ k.

Set R to be the term ⋃_{k ∈ ω}R_ k.

We will prove SNoCut L R ∈ real.

We prove the intermediate claim L_L_R_real: ∀k, nat_p k → L_ k ⊆ real ∧ R_ k ⊆ real.

We will prove ∀k, nat_p k → SNo_sqrtaux x sqrt_SNo_nonneg k 0 ⊆ real ∧ SNo_sqrtaux x sqrt_SNo_nonneg k 1 ⊆ real.

Apply nat_ind to the current goal.

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

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

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

Apply andI to the current goal.

We will prove {sqrt_SNo_nonneg w|w ∈ SNoL_nonneg x} ⊆ real.

Let w' be given.

Assume Hw'.

Apply ReplE_impred (SNoL_nonneg x) sqrt_SNo_nonneg w' Hw' to the current goal.

Let w be given.

Assume Hw: w ∈ SNoL_nonneg x.

Assume Hw'w: w' = sqrt_SNo_nonneg w.

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

We will prove sqrt_SNo_nonneg w ∈ real.

Apply SepE (SNoL x) (λw ⇒ 0 ≤ w) w Hw to the current goal.

Assume Hw1: w ∈ SNoL x.

Assume Hwnneg: 0 ≤ w.

Apply SNoL_E x Hx w Hw1 to the current goal.

Assume Hw1a Hw1b Hw1c.

Apply IH to the current goal.

We will prove w ∈ SNoS_ (SNoLev x).

An exact proof term for the current goal is SNoS_I2 w x Hw1a Hx Hw1b.

We will prove SNoLev w ∈ ω.

An exact proof term for the current goal is omega_TransSet (SNoLev x) Hx1 (SNoLev w) Hw1b.

We will prove 0 ≤ w.

An exact proof term for the current goal is Hwnneg.

We will prove {sqrt_SNo_nonneg z|z ∈ SNoR x} ⊆ real.

Let z' be given.

Assume Hz'.

Apply ReplE_impred (SNoR x) sqrt_SNo_nonneg z' Hz' to the current goal.

Let z be given.

Assume Hz: z ∈ SNoR x.

Assume Hz'z: z' = sqrt_SNo_nonneg z.

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

We will prove sqrt_SNo_nonneg z ∈ real.

Apply SNoR_E x Hx z Hz to the current goal.

Assume Hz1 Hz2 Hz3.

Apply IH to the current goal.

We will prove z ∈ SNoS_ (SNoLev x).

An exact proof term for the current goal is SNoS_I2 z x Hz1 Hx Hz2.

We will prove SNoLev z ∈ ω.

An exact proof term for the current goal is omega_TransSet (SNoLev x) Hx1 (SNoLev z) Hz2.

We will prove 0 ≤ z.

Apply SNoLtLe to the current goal.

We will prove 0 < z.

Apply SNoLeLt_tra 0 x z SNo_0 Hx Hz1 Hx2 to the current goal.

We will prove x < z.

An exact proof term for the current goal is Hz3.

Let k be given.

Assume Hk.

Assume IHk.

Apply IHk to the current goal.

Assume IHk0: SNo_sqrtaux x sqrt_SNo_nonneg k 0 ⊆ real.

Assume IHk1: SNo_sqrtaux x sqrt_SNo_nonneg k 1 ⊆ real.

rewrite the current goal using SNo_sqrtaux_S x sqrt_SNo_nonneg k Hk (from left to right).

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

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

Apply andI to the current goal.

We will prove SNo_sqrtaux x sqrt_SNo_nonneg k 0 ∪ SNo_sqrtauxset (SNo_sqrtaux x sqrt_SNo_nonneg k 0) (SNo_sqrtaux x sqrt_SNo_nonneg k 1) x ⊆ real.

Apply binunion_Subq_min to the current goal.

An exact proof term for the current goal is IHk0.

We will prove SNo_sqrtauxset (SNo_sqrtaux x sqrt_SNo_nonneg k 0) (SNo_sqrtaux x sqrt_SNo_nonneg k 1) x ⊆ real.

Apply SNo_sqrtauxset_real to the current goal.

An exact proof term for the current goal is IHk0.

An exact proof term for the current goal is IHk1.

An exact proof term for the current goal is Lx.

We will prove SNo_sqrtaux x sqrt_SNo_nonneg k 1 ∪ SNo_sqrtauxset (SNo_sqrtaux x sqrt_SNo_nonneg k 0) (SNo_sqrtaux x sqrt_SNo_nonneg k 0) x ∪ SNo_sqrtauxset (SNo_sqrtaux x sqrt_SNo_nonneg k 1) (SNo_sqrtaux x sqrt_SNo_nonneg k 1) x ⊆ real.

Apply binunion_Subq_min to the current goal.

An exact proof term for the current goal is IHk1.

We will prove SNo_sqrtauxset (SNo_sqrtaux x sqrt_SNo_nonneg k 0) (SNo_sqrtaux x sqrt_SNo_nonneg k 0) x ⊆ real.

Apply SNo_sqrtauxset_real to the current goal.

An exact proof term for the current goal is IHk0.

An exact proof term for the current goal is Lx.

We will prove SNo_sqrtauxset (SNo_sqrtaux x sqrt_SNo_nonneg k 1) (SNo_sqrtaux x sqrt_SNo_nonneg k 1) x ⊆ real.

Apply SNo_sqrtauxset_real to the current goal.

An exact proof term for the current goal is IHk1.

An exact proof term for the current goal is Lx.

We prove the intermediate claim L1L: ∀w ∈ L, ∀p : prop, (SNo w → 0 ≤ w → w * w < x → p) → p.

Let w be given.

Assume Hw.

Let p be given.

Assume Hp.

Apply famunionE_impred ω L_ w Hw to the current goal.

Let k be given.

Assume Hk: k ∈ ω.

Assume H1: w ∈ L_ k.

Apply SNo_sqrtaux_0_prop x Hx Hx2 k (omega_nat_p k Hk) w H1 to the current goal.

Assume H2.

Apply H2 to the current goal.

An exact proof term for the current goal is Hp.

We prove the intermediate claim L1R: ∀z ∈ R, ∀p : prop, (SNo z → 0 ≤ z → x < z * z → p) → p.

Let z be given.

Assume Hz.

Let p be given.

Assume Hp.

Apply famunionE_impred ω R_ z Hz to the current goal.

Let k be given.

Assume Hk: k ∈ ω.

Assume H1: z ∈ R_ k.

Apply SNo_sqrtaux_1_prop x Hx Hx2 k (omega_nat_p k Hk) z H1 to the current goal.

Assume H3.

Apply H3 to the current goal.

An exact proof term for the current goal is Hp.

We prove the intermediate claim LLR: SNoCutP L R.

An exact proof term for the current goal is SNo_sqrt_SNo_SNoCutP x Hx Hx2.

Apply LLR to the current goal.

Assume HLHR.

Apply HLHR to the current goal.

Assume HL: ∀w ∈ L, SNo w.

Assume HR: ∀z ∈ R, SNo z.

Assume HLR: ∀w ∈ L, ∀z ∈ R, w < z.

Apply real_SNoCut to the current goal.

We will prove L ⊆ real.

Let w be given.

Assume Hw: w ∈ L.

Apply famunionE_impred ω L_ w Hw to the current goal.

Let k be given.

Assume Hk: k ∈ ω.

Assume H1: w ∈ L_ k.

Apply L_L_R_real k (omega_nat_p k Hk) to the current goal.

Assume H2 _.

An exact proof term for the current goal is H2 w H1.

We will prove R ⊆ real.

Let z be given.

Assume Hz: z ∈ R.

Apply famunionE_impred ω R_ z Hz to the current goal.

Let k be given.

Assume Hk: k ∈ ω.

Assume H1: z ∈ R_ k.

Apply L_L_R_real k (omega_nat_p k Hk) to the current goal.

Assume _ H2.

An exact proof term for the current goal is H2 z H1.

We will prove SNoCutP L R.

An exact proof term for the current goal is LLR.

We will prove L ≠ 0.

An exact proof term for the current goal is sqrt_SNo_nonneg_Lnonempty x Hx Hx2 H1.

We will prove R ≠ 0.

An exact proof term for the current goal is sqrt_SNo_nonneg_Rnonempty x Hx Hx2 H2.

We will prove ∀w ∈ L, ∃w' ∈ L, w < w'.

Let w be given.

Assume Hw.

Apply famunionE_impred ω L_ w Hw to the current goal.

Let k be given.

Assume Hk: k ∈ ω.

Assume H3: w ∈ L_ k.

Apply L1L w Hw to the current goal.

Assume Hw1: SNo w.

Assume Hw2: 0 ≤ w.

Assume Hw3: w * w < x.

We prove the intermediate claim Lwmw: SNo (w * w).

An exact proof term for the current goal is SNo_mul_SNo w w Hw1 Hw1.

We prove the intermediate claim Lwpw: SNo (w + w).

An exact proof term for the current goal is SNo_add_SNo w w Hw1 Hw1.

We prove the intermediate claim L1a: ∃z, z ∈ R_ (ordsucc k).

Apply SNoLt_trichotomy_or_impred x 1 Hx SNo_1 to the current goal.

Assume H4: x < 1.

We use 1 to witness the existential quantifier.

We will prove 1 ∈ R_ (ordsucc k).

Apply SNo_sqrtaux_mon x sqrt_SNo_nonneg 0 nat_0 (ordsucc k) (nat_ordsucc k (omega_nat_p k Hk)) (Subq_Empty (ordsucc k)) to the current goal.

Assume _.

Assume H5: ∀z ∈ R_ 0, z ∈ R_ (ordsucc k).

We will prove 1 ∈ R_ (ordsucc k).

Apply H5 to the current goal.

We will prove 1 ∈ R_ 0.

We will prove 1 ∈ SNo_sqrtaux x sqrt_SNo_nonneg 0 1.

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

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

We will prove 1 ∈ {sqrt_SNo_nonneg z|z ∈ SNoR x}.

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

Apply ReplI to the current goal.

We will prove 1 ∈ SNoR x.

We will prove 1 ∈ {z ∈ SNoS_ (SNoLev x)|x < z}.

Apply SepI to the current goal.

We will prove 1 ∈ SNoS_ (SNoLev x).

Apply SNoS_I2 1 x SNo_1 Hx to the current goal.

We will prove SNoLev 1 ∈ SNoLev x.

rewrite the current goal using ordinal_SNoLev 1 ordinal_1 (from left to right).

An exact proof term for the current goal is H2.

We will prove x < 1.

An exact proof term for the current goal is H4.

Assume H4: x = 1.

We will prove False.

Apply In_irref 1 to the current goal.

We will prove 1 ∈ 1.

rewrite the current goal using ordinal_SNoLev 1 ordinal_1 (from right to left) at position 2.

We will prove 1 ∈ SNoLev 1.

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

An exact proof term for the current goal is H2.

Assume H4: 1 < x.

We prove the intermediate claim L1a1: 1 ∈ L_ k.

Apply SNo_sqrtaux_mon x sqrt_SNo_nonneg 0 nat_0 k (omega_nat_p k Hk) (Subq_Empty k) to the current goal.

Assume H5: ∀z ∈ L_ 0, z ∈ L_ k.

Assume _.

We will prove 1 ∈ L_ k.

Apply H5 to the current goal.

We will prove 1 ∈ L_ 0.

We will prove 1 ∈ SNo_sqrtaux x sqrt_SNo_nonneg 0 0.

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

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

We will prove 1 ∈ {sqrt_SNo_nonneg z|z ∈ SNoL_nonneg x}.

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

Apply ReplI to the current goal.

We will prove 1 ∈ SNoL_nonneg x.

We will prove 1 ∈ {w ∈ SNoL x|0 ≤ w}.

Apply SepI to the current goal.

We will prove 1 ∈ {z ∈ SNoS_ (SNoLev x)|z < x}.

Apply SepI to the current goal.

We will prove 1 ∈ SNoS_ (SNoLev x).

Apply SNoS_I2 1 x SNo_1 Hx to the current goal.

We will prove SNoLev 1 ∈ SNoLev x.

rewrite the current goal using ordinal_SNoLev 1 ordinal_1 (from left to right).

An exact proof term for the current goal is H2.

We will prove 1 < x.

An exact proof term for the current goal is H4.

We will prove 0 ≤ 1.

Apply SNoLtLe to the current goal.

An exact proof term for the current goal is SNoLt_0_1.

We prove the intermediate claim L1a2: 0 < 1 + 1.

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

An exact proof term for the current goal is SNoLt_0_2.

Set z to be the term (x + 1 * 1) :/: (1 + 1).

We use z to witness the existential quantifier.

We will prove z ∈ R_ (ordsucc k).

We will prove z ∈ SNo_sqrtaux x sqrt_SNo_nonneg (ordsucc k) 1.

rewrite the current goal using SNo_sqrtaux_S x sqrt_SNo_nonneg k (omega_nat_p k Hk) (from left to right).

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

We will prove z ∈ R_ k ∪ SNo_sqrtauxset (L_ k) (L_ k) x ∪ SNo_sqrtauxset (R_ k) (R_ k) x.

Apply binunionI1 to the current goal.

Apply binunionI2 to the current goal.

We will prove z ∈ SNo_sqrtauxset (L_ k) (L_ k) x.

An exact proof term for the current goal is SNo_sqrtauxset_I (L_ k) (L_ k) x 1 L1a1 1 L1a1 L1a2.

Apply L1a to the current goal.

Let z be given.

Assume Hz: z ∈ R_ (ordsucc k).

We prove the intermediate claim Lz: z ∈ R.

An exact proof term for the current goal is famunionI ω R_ (ordsucc k) z (omega_ordsucc k Hk) Hz.

Apply L1R z Lz to the current goal.

Assume Hz1: SNo z.

Assume Hz2: 0 ≤ z.

Assume Hz3: x < z * z.

We prove the intermediate claim Lwmz: SNo (w * z).

An exact proof term for the current goal is SNo_mul_SNo w z Hw1 Hz1.

We prove the intermediate claim Lwpz: SNo (w + z).

An exact proof term for the current goal is SNo_add_SNo w z Hw1 Hz1.

We prove the intermediate claim Lzpos: 0 < z.

Apply SNoLeE 0 z SNo_0 Hz1 Hz2 to the current goal.

Assume H4: 0 < z.

An exact proof term for the current goal is H4.

Assume H4: 0 = z.

We will prove False.

Apply SNoLt_irref 0 to the current goal.

We will prove 0 < 0.

Apply SNoLeLt_tra 0 x 0 SNo_0 Hx SNo_0 Hx2 to the current goal.

We will prove x < 0.

rewrite the current goal using mul_SNo_zeroR 0 SNo_0 (from right to left).

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

We will prove x < z * z.

An exact proof term for the current goal is Hz3.

We prove the intermediate claim Lwpzpos: 0 < w + z.

Apply SNoLtLe_tra 0 z (w + z) SNo_0 Hz1 Lwpz Lzpos to the current goal.

We will prove z ≤ w + z.

rewrite the current goal using add_SNo_0L z Hz1 (from right to left) at position 1.

We will prove 0 + z ≤ w + z.

An exact proof term for the current goal is add_SNo_Le1 0 z w SNo_0 Hz1 Hw1 Hw2.

We prove the intermediate claim Lwpzn0: w + z ≠ 0.

Assume H4: w + z = 0.

Apply SNoLt_irref 0 to the current goal.

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

An exact proof term for the current goal is Lwpzpos.

Set w' to be the term (x + w * z) :/: (w + z).

We prove the intermediate claim Lw': w' ∈ L_ (ordsucc (ordsucc k)).

We will prove w' ∈ SNo_sqrtaux x sqrt_SNo_nonneg (ordsucc (ordsucc k)) 0.

rewrite the current goal using SNo_sqrtaux_S x sqrt_SNo_nonneg (ordsucc k) (nat_ordsucc k (omega_nat_p k Hk)) (from left to right).

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

We will prove w' ∈ L_ (ordsucc k) ∪ SNo_sqrtauxset (L_ (ordsucc k)) (R_ (ordsucc k)) x.

Apply binunionI2 to the current goal.

We will prove w' ∈ SNo_sqrtauxset (L_ (ordsucc k)) (R_ (ordsucc k)) x.

We will prove (x + w * z) :/: (w + z) ∈ SNo_sqrtauxset (L_ (ordsucc k)) (R_ (ordsucc k)) x.

We prove the intermediate claim LwLk: w ∈ L_ (ordsucc k).

We will prove w ∈ L_ (ordsucc k).

Apply SNo_sqrtaux_mon x sqrt_SNo_nonneg k (omega_nat_p k Hk) (ordsucc k) (nat_ordsucc k (omega_nat_p k Hk)) (ordsuccI1 k) to the current goal.

Assume H5: ∀u ∈ L_ k, u ∈ L_ (ordsucc k).

Assume _.

Apply H5 to the current goal.

We will prove w ∈ L_ k.

An exact proof term for the current goal is H3.

An exact proof term for the current goal is SNo_sqrtauxset_I (L_ (ordsucc k)) (R_ (ordsucc k)) x w LwLk z Hz Lwpzpos.

We use w' to witness the existential quantifier.

Apply andI to the current goal.

We will prove w' ∈ L.

An exact proof term for the current goal is famunionI ω L_ (ordsucc (ordsucc k)) w' (omega_ordsucc (ordsucc k) (omega_ordsucc k Hk)) Lw'.

We will prove w < w'.

rewrite the current goal using div_mul_SNo_invL w (w + z) Hw1 Lwpz Lwpzn0 (from right to left) at position 1.

We will prove (w * (w + z)) :/: (w + z) < w'.

We will prove (w * (w + z)) * recip_SNo (w + z) < (x + w * z) * recip_SNo (w + z).

Apply pos_mul_SNo_Lt' (w * (w + z)) (x + w * z) (recip_SNo (w + z)) (SNo_mul_SNo w (w + z) Hw1 Lwpz) (SNo_add_SNo x (w * z) Hx Lwmz) (SNo_recip_SNo (w + z) Lwpz) (recip_SNo_of_pos_is_pos (w + z) Lwpz Lwpzpos) to the current goal.

We will prove w * (w + z) < x + w * z.

rewrite the current goal using mul_SNo_distrL w w z Hw1 Hw1 Hz1 (from left to right).

We will prove w * w + w * z < x + w * z.

Apply add_SNo_Lt1 (w * w) (w * z) x Lwmw Lwmz Hx to the current goal.

We will prove w * w < x.

An exact proof term for the current goal is Hw3.

We will prove ∀z ∈ R, ∃z' ∈ R, z' < z.

Let z be given.

Assume Hz.

Apply famunionE_impred ω R_ z Hz to the current goal.

Let k be given.

Assume Hk: k ∈ ω.

Assume H3: z ∈ R_ k.

Apply L1R z Hz to the current goal.

Assume Hz1: SNo z.

Assume Hz2: 0 ≤ z.

Assume Hz3: x < z * z.

We prove the intermediate claim Lzmz: SNo (z * z).

An exact proof term for the current goal is SNo_mul_SNo z z Hz1 Hz1.

We prove the intermediate claim Lzpz: SNo (z + z).

An exact proof term for the current goal is SNo_add_SNo z z Hz1 Hz1.

We prove the intermediate claim Lzpos: 0 < z.

Apply SNoLeE 0 z SNo_0 Hz1 Hz2 to the current goal.

Assume H4: 0 < z.

An exact proof term for the current goal is H4.

Assume H4: 0 = z.

We will prove False.

Apply SNoLt_irref 0 to the current goal.

We will prove 0 < 0.

Apply SNoLeLt_tra 0 x 0 SNo_0 Hx SNo_0 Hx2 to the current goal.

We will prove x < 0.

rewrite the current goal using mul_SNo_zeroR 0 SNo_0 (from right to left).

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

We will prove x < z * z.

An exact proof term for the current goal is Hz3.

We prove the intermediate claim Lzpzpos: 0 < z + z.

rewrite the current goal using add_SNo_0L 0 SNo_0 (from right to left).

An exact proof term for the current goal is add_SNo_Lt3 0 0 z z SNo_0 SNo_0 Hz1 Hz1 Lzpos Lzpos.

We prove the intermediate claim Lzpzn0: z + z ≠ 0.

Assume H4: z + z = 0.

Apply SNoLt_irref 0 to the current goal.

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

An exact proof term for the current goal is Lzpzpos.

Set z' to be the term (x + z * z) :/: (z + z).

We prove the intermediate claim Lz': z' ∈ R_ (ordsucc k).

We will prove z' ∈ SNo_sqrtaux x sqrt_SNo_nonneg (ordsucc k) 1.

rewrite the current goal using SNo_sqrtaux_S x sqrt_SNo_nonneg k (omega_nat_p k Hk) (from left to right).

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

We will prove z' ∈ R_ k ∪ SNo_sqrtauxset (L_ k) (L_ k) x ∪ SNo_sqrtauxset (R_ k) (R_ k) x.

Apply binunionI2 to the current goal.

We will prove z' ∈ SNo_sqrtauxset (R_ k) (R_ k) x.

Apply SNo_sqrtauxset_I to the current goal.

We will prove z ∈ R_ k.

An exact proof term for the current goal is H3.

We will prove z ∈ R_ k.

An exact proof term for the current goal is H3.

We will prove 0 < z + z.

An exact proof term for the current goal is Lzpzpos.

We use z' to witness the existential quantifier.

Apply andI to the current goal.

We will prove z' ∈ R.

An exact proof term for the current goal is famunionI ω R_ (ordsucc k) z' (omega_ordsucc k Hk) Lz'.

We will prove z' < z.

rewrite the current goal using div_mul_SNo_invL z (z + z) Hz1 Lzpz Lzpzn0 (from right to left) at position 5.

We will prove z' < (z * (z + z)) :/: (z + z).

We will prove (x + z * z) * recip_SNo (z + z) < (z * (z + z)) * recip_SNo (z + z).

Apply pos_mul_SNo_Lt' (x + z * z) (z * (z + z)) (recip_SNo (z + z)) (SNo_add_SNo x (z * z) Hx Lzmz) (SNo_mul_SNo z (z + z) Hz1 Lzpz) (SNo_recip_SNo (z + z) Lzpz) (recip_SNo_of_pos_is_pos (z + z) Lzpz Lzpzpos) to the current goal.

We will prove x + z * z < z * (z + z).

rewrite the current goal using mul_SNo_distrL z z z Hz1 Hz1 Hz1 (from left to right).

We will prove x + z * z < z * z + z * z.

Apply add_SNo_Lt1 x (z * z) (z * z) Hx Lzmz Lzmz to the current goal.

We will prove x < z * z.

An exact proof term for the current goal is Hz3.

Assume H2: SNoLev x ⊆ 1.

We prove the intermediate claim L1_1: x = 1.

Use symmetry.

Apply SNo_eq 1 x SNo_1 Hx to the current goal.

We will prove SNoLev 1 = SNoLev x.

rewrite the current goal using ordinal_SNoLev 1 ordinal_1 (from left to right).

We will prove 1 = SNoLev x.

Apply set_ext to the current goal.

Let u be given.

Assume Hu: u ∈ 1.

Apply cases_1 u Hu to the current goal.

We will prove 0 ∈ SNoLev x.

An exact proof term for the current goal is H1.

An exact proof term for the current goal is H2.

We will prove SNoEq_ (SNoLev 1) 1 x.

rewrite the current goal using ordinal_SNoLev 1 ordinal_1 (from left to right).

We will prove SNoEq_ 1 1 x.

Let u be given.

Assume Hu: u ∈ 1.

We will prove u ∈ 1 ↔ u ∈ x.

Apply iffI to the current goal.

Assume _.

Apply cases_1 u Hu to the current goal.

We will prove 0 ∈ x.

Apply dneg to the current goal.

Assume H3: 0 ∉ x.

Apply SNoLt_irref 0 to the current goal.

We will prove 0 < 0.

Apply SNoLeLt_tra 0 x 0 SNo_0 Hx SNo_0 Hx2 to the current goal.

We will prove x < 0.

Apply SNoLtI3 to the current goal.

We will prove SNoLev 0 ∈ SNoLev x.

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

An exact proof term for the current goal is H1.

We will prove SNoEq_ (SNoLev 0) x 0.

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

Let u be given.

Assume Hu: u ∈ 0.

We will prove False.

An exact proof term for the current goal is EmptyE u Hu.

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

An exact proof term for the current goal is H3.

Assume _.

An exact proof term for the current goal is Hu.

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

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

We will prove 1 ∈ real.

An exact proof term for the current goal is real_1.

Assume H1: SNoLev x ⊆ 0.

We prove the intermediate claim L1_0: x = 0.

Apply SNoLev_0_eq_0 x Hx to the current goal.

We will prove SNoLev x = 0.

Apply Empty_Subq_eq to the current goal.

An exact proof term for the current goal is H1.

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

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

We will prove 0 ∈ real.

An exact proof term for the current goal is real_0.