rewrite the current goal using sqrt_SNo_nonneg_eq 0 SNo_0 (from left to right).
Set L_ to be the term λk : set ⇒ SNo_sqrtaux 0 sqrt_SNo_nonneg k 0.
Set R_ to be the term λk : set ⇒ SNo_sqrtaux 0 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 = 0.
We prove the intermediate claim L1: ∀k, nat_p k → L_ k = 0 ∧ R_ k = 0.
Apply nat_ind to the current goal.
Apply andI to the current goal.
We will prove L_ 0 = 0.
We will prove SNo_sqrtaux 0 sqrt_SNo_nonneg 0 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 {sqrt_SNo_nonneg w|w ∈ SNoL_nonneg 0} = 0.
rewrite the current goal using SNoL_nonneg_0 (from left to right).
An exact proof term for the current goal is Repl_Empty sqrt_SNo_nonneg.
We will prove R_ 0 = 0.
We will prove SNo_sqrtaux 0 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 0} = 0.
rewrite the current goal using SNoR_0 (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 = 0.
Assume IHRk: R_ k = 0.
Apply andI to the current goal.
We will prove L_ (ordsucc k) = 0.
We will prove SNo_sqrtaux 0 sqrt_SNo_nonneg (ordsucc k) 0 = 0.
rewrite the current goal using SNo_sqrtaux_S 0 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) 0 = Empty.
rewrite the current goal using IHLk (from left to right).
We will prove 0 ∪ SNo_sqrtauxset 0 (R_ k) 0 = Empty.
Apply SNo_sqrtauxset_0 (R_ k) 0 (λ_ u ⇒ 0 ∪ u = 0) to the current goal.
We will prove 0 ∪ 0 = Empty.
Apply binunion_idl to the current goal.
We will prove R_ (ordsucc k) = 0.
We will prove SNo_sqrtaux 0 sqrt_SNo_nonneg (ordsucc k) 1 = 0.
rewrite the current goal using SNo_sqrtaux_S 0 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) 0 ∪ SNo_sqrtauxset (R_ k) (R_ k) 0 = Empty.
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 0 0 0 ∪ SNo_sqrtauxset 0 0 0 = Empty.
rewrite the current goal using SNo_sqrtauxset_0 0 0 (from left to right).
We will prove 0 ∪ 0 ∪ 0 = Empty.
rewrite the current goal using binunion_idl 0 (from left to right).
We will prove 0 ∪ 0 = Empty.
Apply binunion_idl to the current goal.
We prove the intermediate claim L2: L = 0.
Apply Empty_eq to the current goal.
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 = 0.
Assume _.
We will prove x ∉ L_ k.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is EmptyE x.
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).
An exact proof term for the current goal is SNoCut_0_0.
∎