Let x be given.
Assume Hx Hxnn H1.
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 L ≠ 0.
Assume H2: L = 0.
We prove the intermediate claim L1: sqrt_SNo_nonneg 0 ∈ L_ 0.
rewrite the current goal using sqrt_SNo_nonneg_0 (from left to right).
An exact proof term for the current goal is sqrt_SNo_nonneg_0inL0 x Hx Hxnn H1.
Apply EmptyE (sqrt_SNo_nonneg 0) to the current goal.
We will prove sqrt_SNo_nonneg 0 ∈ 0.
rewrite the current goal using H2 (from right to left) at position 2.
An exact proof term for the current goal is famunionI ω L_ 0 (sqrt_SNo_nonneg 0) (nat_p_omega 0 nat_0) L1.
∎