Let x be given.
Assume Hx Hxnonneg H1 H1R.
rewrite the current goal using SNoCut_0_0 (from right to left) at position 1.
Set L_ to be the term λk ⇒ SNo_sqrtaux x sqrt_SNo_nonneg k 0 of type set → set.
Set R_ to be the term λk ⇒ SNo_sqrtaux x sqrt_SNo_nonneg k 1 of type set → set.
Set L to be the term ⋃k ∈ ωL_ k.
Set R to be the term ⋃k ∈ ωR_ k.
We will prove SNoCut 0 0 ≤ SNoCut L R.
Apply SNoCut_Le 0 0 L R to the current goal.
We will prove SNoCutP 0 0.
An exact proof term for the current goal is SNoCutP_0_0.
An exact proof term for the current goal is H1.
Let w be given.
Assume Hw: w ∈ 0.
We will prove False.
An exact proof term for the current goal is EmptyE w Hw.
Let z be given.
Assume Hz: z ∈ R.
We will prove SNoCut 0 0 < z.
rewrite the current goal using SNoCut_0_0 (from left to right).
We will prove 0 < z.
Apply H1R z Hz to the current goal.
Assume Hz1: SNo z.
Assume Hz2: 0 ≤ z.
Assume Hz3: x < z * z.
Apply SNoLeE 0 z SNo_0 Hz1 Hz2 to the current goal.
Assume H6: 0 < z.
An exact proof term for the current goal is H6.
Assume H6: 0 = z.
We will prove False.
Apply SNoLt_irref x to the current goal.
We will prove x < x.
Apply SNoLtLe_tra x 0 x Hx SNo_0 Hx to the current goal.
We will prove x < 0.
rewrite the current goal using mul_SNo_zeroR 0 SNo_0 (from right to left).
We will prove x < 0 * 0.
rewrite the current goal using H6 (from left to right).
An exact proof term for the current goal is Hz3.
We will prove 0 ≤ x.
An exact proof term for the current goal is Hxnonneg.
∎