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 R ≠ 0.
Assume H2: R = 0.
Apply SNoLt_trichotomy_or_impred x 1 Hx SNo_1 to the current goal.
Assume H3: x < 1.
We prove the intermediate claim L1: 1 ∈ SNoR x.
Apply SNoR_I x Hx 1 SNo_1 to the current goal.
We will prove SNoLev 1 ∈ SNoLev x.
rewrite the current goal using ordinal_SNoLev 1 (nat_p_ordinal 1 nat_1) (from left to right).
An exact proof term for the current goal is H1.
An exact proof term for the current goal is H3.
We prove the intermediate claim L2: sqrt_SNo_nonneg 1 ∈ R_ 0.
We will prove sqrt_SNo_nonneg 1 ∈ SNo_sqrtaux x sqrt_SNo_nonneg 0 1.
rewrite the current goal using SNo_sqrtaux_0 x sqrt_SNo_nonneg (from left to right).
rewrite the current goal using tuple_2_1_eq (from left to right).
We will prove sqrt_SNo_nonneg 1 ∈ {sqrt_SNo_nonneg z|z ∈ SNoR x}.
Apply ReplI to the current goal.
An exact proof term for the current goal is L1.
Apply EmptyE (sqrt_SNo_nonneg 1) to the current goal.
rewrite the current goal using H2 (from right to left) at position 2.
We will prove sqrt_SNo_nonneg 1 ∈ R.
An exact proof term for the current goal is famunionI ω R_ 0 (sqrt_SNo_nonneg 1) (nat_p_omega 0 nat_0) L2.
Assume H3: 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 (nat_p_ordinal 1 nat_1) (from right to left) at position 2.
rewrite the current goal using H3 (from right to left) at position 2.
An exact proof term for the current goal is H1.
Assume H3: 1 < x.
We prove the intermediate claim L3: 1 ∈ SNoL_nonneg x.
We will prove 1 ∈ {w ∈ SNoL x|0 ≤ w}.
Apply SepI to the current goal.
Apply SNoL_I x Hx 1 SNo_1 to the current goal.
We will prove SNoLev 1 ∈ SNoLev x.
rewrite the current goal using ordinal_SNoLev 1 (nat_p_ordinal 1 nat_1) (from left to right).
An exact proof term for the current goal is H1.
An exact proof term for the current goal is H3.
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 L4: (x + 1 * 0) :/: (1 + 0) ∈ R_ 1.
We will prove (x + 1 * 0) :/: (1 + 0) ∈ SNo_sqrtaux x sqrt_SNo_nonneg 1 1.
rewrite the current goal using SNo_sqrtaux_S x sqrt_SNo_nonneg 0 nat_0 (from left to right).
rewrite the current goal using tuple_2_1_eq (from left to right).
Apply binunionI1 to the current goal.
Apply binunionI2 to the current goal.
Apply SNo_sqrtauxset_I 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 w|w ∈ 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.
An exact proof term for the current goal is L3.
We will prove 0 ∈ L_ 0.
An exact proof term for the current goal is sqrt_SNo_nonneg_0inL0 x Hx Hxnn (ordinal_TransSet (SNoLev x) (SNoLev_ordinal x Hx) 1 H1 0 In_0_1).
We will prove 0 < 1 + 0.
rewrite the current goal using add_SNo_0R 1 SNo_1 (from left to right).
An exact proof term for the current goal is SNoLt_0_1.
Apply EmptyE ((x + 1 * 0) :/: (1 + 0)) to the current goal.
rewrite the current goal using H2 (from right to left) at position 5.
We will prove ((x + 1 * 0) :/: (1 + 0)) ∈ R.
An exact proof term for the current goal is famunionI ω R_ 1 ((x + 1 * 0) :/: (1 + 0)) (nat_p_omega 1 nat_1) L4.
∎