rewrite the current goal using sqrt_SNo_nonneg_eq 1 SNo_1 (from left to right).
Set L_ to be the term λk : set ⇒ SNo_sqrtaux 1 sqrt_SNo_nonneg k 0.
Set R_ to be the term λk : set ⇒ SNo_sqrtaux 1 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 = 1.
We prove the intermediate claim L1: ∀k, nat_p k → L_ k = 1 ∧ R_ k = 0.
Apply nat_ind to the current goal.
Apply andI to the current goal.
We will prove L_ 0 = 1.
We will prove SNo_sqrtaux 1 sqrt_SNo_nonneg 0 0 = 1.
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 {sqrt_SNo_nonneg w|w ∈ SNoL_nonneg 1} = 1.
rewrite the current goal using SNoL_nonneg_1 (from left to right).
We will prove {sqrt_SNo_nonneg w|w ∈ 1} = 1.
Apply set_ext to the current goal.
Let u be given.
Assume Hu: u ∈ {sqrt_SNo_nonneg w|w ∈ 1}.
We will prove u ∈ 1.
Apply ReplE_impred 1 sqrt_SNo_nonneg u Hu to the current goal.
Let w be given.
Assume Hw: w ∈ 1.
Apply cases_1 w Hw to the current goal.
rewrite the current goal using sqrt_SNo_nonneg_0 (from left to right).
Assume Hu0: u = 0.
rewrite the current goal using Hu0 (from left to right).
An exact proof term for the current goal is In_0_1.
Let u be given.
Assume Hu: u ∈ 1.
Apply cases_1 u Hu to the current goal.
We will prove 0 ∈ {sqrt_SNo_nonneg w|w ∈ 1}.
rewrite the current goal using sqrt_SNo_nonneg_0 (from right to left) at position 1.
Apply ReplI to the current goal.
An exact proof term for the current goal is In_0_1.
We will prove R_ 0 = 0.
We will prove SNo_sqrtaux 1 sqrt_SNo_nonneg 0 1 = 0.
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 {sqrt_SNo_nonneg w|w ∈ SNoR 1} = 0.
rewrite the current goal using SNoR_1 (from left to right).
An exact proof term for the current goal is Repl_Empty sqrt_SNo_nonneg.
Let k be given.
Assume Hk.
Assume IHk.
Apply IHk to the current goal.
Assume IHLk: L_ k = 1.
Assume IHRk: R_ k = 0.
Apply andI to the current goal.
We will prove L_ (ordsucc k) = 1.
We will prove SNo_sqrtaux 1 sqrt_SNo_nonneg (ordsucc k) 0 = 1.
rewrite the current goal using SNo_sqrtaux_S 1 sqrt_SNo_nonneg k Hk (from left to right).
rewrite the current goal using tuple_2_0_eq (from left to right).
We will prove L_ k ∪ SNo_sqrtauxset (L_ k) (R_ k) 1 = 1.
rewrite the current goal using IHLk (from left to right).
rewrite the current goal using IHRk (from left to right).
We will prove 1 ∪ SNo_sqrtauxset 1 0 1 = 1.
rewrite the current goal using SNo_sqrtauxset_0' 1 1 (from left to right).
Apply binunion_idr to the current goal.
We will prove R_ (ordsucc k) = 0.
We will prove SNo_sqrtaux 1 sqrt_SNo_nonneg (ordsucc k) 1 = 0.
rewrite the current goal using SNo_sqrtaux_S 1 sqrt_SNo_nonneg k Hk (from left to right).
rewrite the current goal using tuple_2_1_eq (from left to right).
We will prove R_ k ∪ SNo_sqrtauxset (L_ k) (L_ k) 1 ∪ SNo_sqrtauxset (R_ k) (R_ k) 1 = 0.
rewrite the current goal using IHLk (from left to right).
rewrite the current goal using IHRk (from left to right).
We will prove 0 ∪ SNo_sqrtauxset 1 1 1 ∪ SNo_sqrtauxset 0 0 1 = 0.
rewrite the current goal using SNo_sqrtauxset_0 0 1 (from left to right).
We will prove 0 ∪ SNo_sqrtauxset 1 1 1 ∪ 0 = 0.
rewrite the current goal using binunion_idl (SNo_sqrtauxset 1 1 1) (from left to right).
rewrite the current goal using binunion_idr (SNo_sqrtauxset 1 1 1) (from left to right).
We will prove SNo_sqrtauxset 1 1 1 = 0.
Apply Empty_eq to the current goal.
Let u be given.
Assume Hu: u ∈ SNo_sqrtauxset 1 1 1.
Apply SNo_sqrtauxset_E 1 1 1 u Hu to the current goal.
Let w be given.
Assume Hw: w ∈ 1.
Let z be given.
Assume Hz: z ∈ 1.
Apply cases_1 w Hw to the current goal.
Apply cases_1 z Hz to the current goal.
rewrite the current goal using add_SNo_0R 0 SNo_0 (from left to right).
Assume H1: 0 < 0.
We will prove False.
Apply SNoLt_irref 0 to the current goal.
An exact proof term for the current goal is H1.
We prove the intermediate claim L2: L = 1.
Apply set_ext to the current goal.
We will prove L ⊆ 1.
Let x be given.
Assume Hx: x ∈ L.
Apply famunionE_impred ω L_ x Hx to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Apply L1 k (omega_nat_p k Hk) to the current goal.
Assume H1: L_ k = 1.
Assume _.
We will prove x ∈ L_ k → x ∈ 1.
rewrite the current goal using H1 (from left to right).
Assume H2: x ∈ 1.
We will prove x ∈ 1.
An exact proof term for the current goal is H2.
Let x be given.
Assume Hx: x ∈ 1.
Apply cases_1 x Hx to the current goal.
We will prove 0 ∈ L.
We prove the intermediate claim L2a: 0 ∈ L_ 0.
Apply L1 0 nat_0 to the current goal.
Assume H1: L_ 0 = 1.
Assume _.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is In_0_1.
We will prove 0 ∈ ⋃k ∈ ωL_ k.
An exact proof term for the current goal is famunionI ω L_ 0 0 (nat_p_omega 0 nat_0) L2a.
We prove the intermediate claim L3: R = 0.
Apply Empty_eq to the current goal.
Let x be given.
Assume Hx: x ∈ R.
Apply famunionE_impred ω R_ x Hx to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Apply L1 k (omega_nat_p k Hk) to the current goal.
Assume _.
Assume H1: R_ k = 0.
We will prove x ∉ R_ k.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is EmptyE x.
rewrite the current goal using L2 (from left to right).
rewrite the current goal using L3 (from left to right).
We will prove SNoCut 1 0 = 1.
rewrite the current goal using SNoL_1 (from right to left) at position 1.
rewrite the current goal using SNoR_1 (from right to left) at position 2.
We will prove SNoCut (SNoL 1) (SNoR 1) = 1.
Use symmetry.
An exact proof term for the current goal is SNo_eta 1 SNo_1.
∎