Let x be given.
Assume Hx Hxnonneg IH HLR.
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.
Set y to be the term SNoCut L R.
Assume Hynn: 0 ≤ y.
Assume H6: x < y * y.
Apply HLR to the current goal.
Assume HLHR.
Apply HLHR to the current goal.
Assume HL: ∀w ∈ L, SNo w.
Assume HR: ∀z ∈ R, SNo z.
Assume HLR': ∀w ∈ L, ∀z ∈ R, w < z.
Apply SNoCutP_SNoCut_impred L R HLR to the current goal.
Assume H1: SNo y.
Assume H2: SNoLev y ∈ ordsucc ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))).
Assume H3: ∀w ∈ L, w < y.
Assume H4: ∀z ∈ R, y < z.
Assume H5: ∀u, SNo u → (∀w ∈ L, w < u) → (∀z ∈ R, u < z) → SNoLev y ⊆ SNoLev u ∧ SNoEq_ (SNoLev y) y u.
We prove the intermediate claim Lyy: SNo (y * y).
An exact proof term for the current goal is SNo_mul_SNo y y H1 H1.
We prove the intermediate claim Lyynn: 0 ≤ y * y.
An exact proof term for the current goal is mul_SNo_nonneg_nonneg y y H1 H1 Hynn Hynn.
We prove the intermediate claim LL_mon: ∀k k', nat_p k → nat_p k' → k ⊆ k' → L_ k ⊆ L_ k'.
Let k and k' be given.
Assume Hk Hk' Hkk'.
Apply SNo_sqrtaux_mon x sqrt_SNo_nonneg k Hk k' Hk' Hkk' to the current goal.
Assume H _.
An exact proof term for the current goal is H.
We prove the intermediate claim LR_mon: ∀k k', nat_p k → nat_p k' → k ⊆ k' → R_ k ⊆ R_ k'.
Let k and k' be given.
Assume Hk Hk' Hkk'.
Apply SNo_sqrtaux_mon x sqrt_SNo_nonneg k Hk k' Hk' Hkk' to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
We prove the intermediate claim L1: ∀k, nat_p k → (∀y ∈ L_ k, SNo y ∧ 0 ≤ y ∧ y * y < x) ∧ (∀y ∈ R_ k, SNo y ∧ 0 ≤ y ∧ x < y * y).
An exact proof term for the current goal is sqrt_SNo_nonneg_prop1a x Hx Hxnonneg IH.
We prove the intermediate claim L1L: ∀w ∈ L, ∀p : prop, (SNo w → 0 ≤ w → w * w < x → p) → p.
Let w be given.
Assume Hw.
Let p be given.
Assume Hp.
Apply famunionE_impred ω L_ w Hw to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume H1: w ∈ L_ k.
Apply L1 k (omega_nat_p k Hk) to the current goal.
Assume H2 _.
Apply H2 w H1 to the current goal.
Assume H3.
Apply H3 to the current goal.
An exact proof term for the current goal is Hp.
We prove the intermediate claim L1R: ∀z ∈ R, ∀p : prop, (SNo z → 0 ≤ z → x < z * z → p) → p.
Let z be given.
Assume Hz.
Let p be given.
Assume Hp.
Apply famunionE_impred ω R_ z Hz to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume H1: z ∈ R_ k.
Apply L1 k (omega_nat_p k Hk) to the current goal.
Assume _ H2.
Apply H2 z H1 to the current goal.
Assume H3.
Apply H3 to the current goal.
An exact proof term for the current goal is Hp.
Apply SNoLtE x (y * y) Hx Lyy H6 to the current goal.
Let u be given.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev x ∩ SNoLev (y * y).
Assume Hu3: SNoEq_ (SNoLev u) u x.
Assume Hu4: SNoEq_ (SNoLev u) u (y * y).
Assume Hu5: x < u.
Assume Hu6: u < y * y.
We will prove False.
We prove the intermediate claim Lunn: 0 ≤ u.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNoLeLt_tra 0 x u SNo_0 Hx Hu1 Hxnonneg Hu5.
We prove the intermediate claim LuSx: u ∈ SNoS_ (SNoLev x).
Apply SNoS_I2 u x Hu1 Hx to the current goal.
We will prove SNoLev u ∈ SNoLev x.
An exact proof term for the current goal is binintersectE1 (SNoLev x) (SNoLev (y * y)) (SNoLev u) Hu2.
Apply IH u LuSx Lunn to the current goal.
Assume H.
Apply H to the current goal.
Assume H7: SNo (sqrt_SNo_nonneg u).
Assume H8: 0 ≤ sqrt_SNo_nonneg u.
Assume H9: sqrt_SNo_nonneg u * sqrt_SNo_nonneg u = u.
We prove the intermediate claim Lysru: y ≤ sqrt_SNo_nonneg u.
Apply SNoLtLe to the current goal.
We will prove y < sqrt_SNo_nonneg u.
Apply H4 to the current goal.
We will prove sqrt_SNo_nonneg u ∈ R.
We prove the intermediate claim Lysru0: sqrt_SNo_nonneg u ∈ R_ 0.
We will prove sqrt_SNo_nonneg u ∈ SNo_sqrtaux x sqrt_SNo_nonneg 0 1.
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 u ∈ {sqrt_SNo_nonneg w|w ∈ SNoR x}.
Apply ReplI to the current goal.
Apply SNoR_I x Hx u Hu1 to the current goal.
An exact proof term for the current goal is binintersectE1 (SNoLev x) (SNoLev (y * y)) (SNoLev u) Hu2.
We will prove x < u.
An exact proof term for the current goal is Hu5.
An exact proof term for the current goal is famunionI ω R_ 0 (sqrt_SNo_nonneg u) (nat_p_omega 0 nat_0) Lysru0.
Apply SNoLt_irref u to the current goal.
We will prove u < u.
Apply SNoLtLe_tra u (y * y) u Hu1 Lyy Hu1 Hu6 to the current goal.
We will prove y * y ≤ u.
rewrite the current goal using H9 (from right to left).
We will prove y * y ≤ sqrt_SNo_nonneg u * sqrt_SNo_nonneg u.
An exact proof term for the current goal is nonneg_mul_SNo_Le2 y y (sqrt_SNo_nonneg u) (sqrt_SNo_nonneg u) H1 H1 H7 H7 Hynn Hynn Lysru Lysru.
Assume H7: SNoLev x ∈ SNoLev (y * y).
Assume H8: SNoEq_ (SNoLev x) x (y * y).
Assume H9: SNoLev x ∈ y * y.
We prove the intermediate claim L10: x ∈ SNoL (y * y).
An exact proof term for the current goal is SNoL_I (y * y) Lyy x Hx H7 H6.
Apply mul_SNo_SNoCut_SNoL_interpolate_impred L R L R HLR HLR y y (λq H ⇒ H) (λq H ⇒ H) x L10 to the current goal.
Let v be given.
Assume Hv: v ∈ L.
Let w be given.
Assume Hw: w ∈ L.
Assume H10: x + v * w ≤ v * y + y * w.
Apply L1L v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: 0 ≤ v.
Assume Hv3: v * v < x.
Apply L1L w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: 0 ≤ w.
Assume Hw3: w * w < x.
Apply SNoLtLe_or 0 (v + w) SNo_0 (SNo_add_SNo v w Hv1 Hw1) to the current goal.
Assume H11: 0 < v + w.
We prove the intermediate claim L11: ∃k, nat_p k ∧ v ∈ L_ k ∧ w ∈ L_ k.
Apply famunionE ω L_ v Hv to the current goal.
Let k' be given.
Assume H.
Apply H to the current goal.
Assume Hk'1: k' ∈ ω.
Assume Hk'2: v ∈ L_ k'.
Apply famunionE ω L_ w Hw to the current goal.
Let k'' be given.
Assume H.
Apply H to the current goal.
Assume Hk''1: k'' ∈ ω.
Assume Hk''2: w ∈ L_ k''.
Apply ordinal_linear k' k'' (nat_p_ordinal k' (omega_nat_p k' Hk'1)) (nat_p_ordinal k'' (omega_nat_p k'' Hk''1)) to the current goal.
Assume H1: k' ⊆ k''.
We use k'' to witness the existential quantifier.
Apply and3I to the current goal.
An exact proof term for the current goal is omega_nat_p k'' Hk''1.
We will prove v ∈ L_ k''.
An exact proof term for the current goal is LL_mon k' k'' (omega_nat_p k' Hk'1) (omega_nat_p k'' Hk''1) H1 v Hk'2.
An exact proof term for the current goal is Hk''2.
Assume H1: k'' ⊆ k'.
We use k' to witness the existential quantifier.
Apply and3I to the current goal.
An exact proof term for the current goal is omega_nat_p k' Hk'1.
An exact proof term for the current goal is Hk'2.
We will prove w ∈ L_ k'.
An exact proof term for the current goal is LL_mon k'' k' (omega_nat_p k'' Hk''1) (omega_nat_p k' Hk'1) H1 w Hk''2.
Apply L11 to the current goal.
Let k be given.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Assume Hk: nat_p k.
Assume Hvk: v ∈ L_ k.
Assume Hwk: w ∈ L_ k.
We prove the intermediate claim Lvw0: v + w ≠ 0.
Assume H.
Apply SNoLt_irref 0 to the current goal.
rewrite the current goal using H (from right to left) at position 2.
An exact proof term for the current goal is H11.
We prove the intermediate claim L12: (x + v * w) :/: (v + w) ∈ R_ (ordsucc k).
We will prove (x + v * w) :/: (v + w) ∈ SNo_sqrtaux x sqrt_SNo_nonneg (ordsucc k) 1.
rewrite the current goal using SNo_sqrtaux_S x 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 (x + v * w) :/: (v + w) ∈ R_ k ∪ SNo_sqrtauxset (L_ k) (L_ k) x ∪ SNo_sqrtauxset (R_ k) (R_ k) x.
Apply binunionI1 to the current goal.
Apply binunionI2 to the current goal.
An exact proof term for the current goal is SNo_sqrtauxset_I (L_ k) (L_ k) x v Hvk w Hwk H11.
We prove the intermediate claim L13: (x + v * w) :/: (v + w) ∈ R.
An exact proof term for the current goal is famunionI ω R_ (ordsucc k) ((x + v * w) :/: (v + w)) (nat_p_omega (ordsucc k) (nat_ordsucc k Hk)) L12.
We prove the intermediate claim L14: y < (x + v * w) :/: (v + w).
An exact proof term for the current goal is H4 ((x + v * w) :/: (v + w)) L13.
We prove the intermediate claim L15: v * y + y * w = y * (v + w).
Use transitivity with and y * v + y * w.
Use f_equal.
We will prove v * y = y * v.
An exact proof term for the current goal is mul_SNo_com v y Hv1 H1.
We will prove y * v + y * w = y * (v + w).
Use symmetry.
An exact proof term for the current goal is mul_SNo_distrL y v w H1 Hv1 Hw1.
We will prove False.
Apply SNoLt_irref (x + v * w) to the current goal.
Apply SNoLeLt_tra (x + v * w) (v * y + y * w) (x + v * w) (SNo_add_SNo x (v * w) Hx (SNo_mul_SNo v w Hv1 Hw1)) (SNo_add_SNo (v * y) (y * w) (SNo_mul_SNo v y Hv1 H1) (SNo_mul_SNo y w H1 Hw1)) (SNo_add_SNo x (v * w) Hx (SNo_mul_SNo v w Hv1 Hw1)) H10 to the current goal.
We will prove v * y + y * w < x + v * w.
rewrite the current goal using L15 (from left to right).
We will prove y * (v + w) < x + v * w.
rewrite the current goal using mul_div_SNo_invL (x + v * w) (v + w) (SNo_add_SNo x (v * w) Hx (SNo_mul_SNo v w Hv1 Hw1)) (SNo_add_SNo v w Hv1 Hw1) Lvw0 (from right to left).
We will prove y * (v + w) < ((x + v * w) :/: (v + w)) * (v + w).
An exact proof term for the current goal is pos_mul_SNo_Lt' y ((x + v * w) :/: (v + w)) (v + w) H1 (SNo_div_SNo (x + v * w) (v + w) (SNo_add_SNo x (v * w) Hx (SNo_mul_SNo v w Hv1 Hw1)) (SNo_add_SNo v w Hv1 Hw1)) (SNo_add_SNo v w Hv1 Hw1) H11 L14.
Assume H11: v + w ≤ 0.
We prove the intermediate claim L16: v = 0 ∧ w = 0.
Apply SNoLtLe_or 0 v SNo_0 Hv1 to the current goal.
Assume H12: 0 < v.
We will prove False.
Apply SNoLt_irref 0 to the current goal.
Apply SNoLtLe_tra 0 v 0 SNo_0 Hv1 SNo_0 H12 to the current goal.
We will prove v ≤ 0.
Apply SNoLe_tra v (v + w) 0 Hv1 (SNo_add_SNo v w Hv1 Hw1) SNo_0 to the current goal.
We will prove v ≤ v + w.
rewrite the current goal using add_SNo_0R v Hv1 (from right to left) at position 1.
We will prove v + 0 ≤ v + w.
An exact proof term for the current goal is add_SNo_Le2 v 0 w Hv1 SNo_0 Hw1 Hw2.
We will prove v + w ≤ 0.
An exact proof term for the current goal is H11.
Assume H12: v ≤ 0.
Apply SNoLtLe_or 0 w SNo_0 Hw1 to the current goal.
Assume H13: 0 < w.
We will prove False.
Apply SNoLt_irref 0 to the current goal.
Apply SNoLtLe_tra 0 w 0 SNo_0 Hw1 SNo_0 H13 to the current goal.
We will prove w ≤ 0.
Apply SNoLe_tra w (v + w) 0 Hw1 (SNo_add_SNo v w Hv1 Hw1) SNo_0 to the current goal.
We will prove w ≤ v + w.
rewrite the current goal using add_SNo_0L w Hw1 (from right to left) at position 1.
We will prove 0 + w ≤ v + w.
An exact proof term for the current goal is add_SNo_Le1 0 w v SNo_0 Hw1 Hv1 Hv2.
We will prove v + w ≤ 0.
An exact proof term for the current goal is H11.
Assume H13: w ≤ 0.
Apply andI to the current goal.
An exact proof term for the current goal is SNoLe_antisym v 0 Hv1 SNo_0 H12 Hv2.
An exact proof term for the current goal is SNoLe_antisym w 0 Hw1 SNo_0 H13 Hw2.
Apply L16 to the current goal.
Assume Hv0: v = 0.
Assume Hw0: w = 0.
We prove the intermediate claim L17: x + v * w = x.
rewrite the current goal using Hv0 (from left to right).
rewrite the current goal using mul_SNo_zeroL w Hw1 (from left to right).
An exact proof term for the current goal is add_SNo_0R x Hx.
We prove the intermediate claim L18: v * y + y * w = 0.
rewrite the current goal using Hv0 (from left to right).
We will prove 0 * y + y * w = 0.
Apply mul_SNo_zeroL y H1 (λ_ u ⇒ u + y * w = 0) to the current goal.
rewrite the current goal using Hw0 (from left to right).
We will prove 0 + y * 0 = 0.
Apply mul_SNo_zeroR y H1 (λ_ u ⇒ 0 + u = 0) to the current goal.
An exact proof term for the current goal is add_SNo_0L 0 SNo_0.
We prove the intermediate claim L19: x ≤ 0.
rewrite the current goal using L17 (from right to left).
rewrite the current goal using L18 (from right to left).
An exact proof term for the current goal is H10.
We prove the intermediate claim L20: x = 0.
An exact proof term for the current goal is SNoLe_antisym x 0 Hx SNo_0 L19 Hxnonneg.
Apply SNoLt_irref (v * v) to the current goal.
We will prove v * v < v * v.
rewrite the current goal using Hv0 (from left to right) at position 3.
We will prove v * v < 0 * v.
rewrite the current goal using mul_SNo_zeroL v Hv1 (from left to right).
We will prove v * v < 0.
rewrite the current goal using L20 (from right to left).
An exact proof term for the current goal is Hv3.
Let v be given.
Assume Hv: v ∈ R.
Let w be given.
Assume Hw: w ∈ R.
Assume H10: x + v * w ≤ v * y + y * w.
Apply L1R v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: 0 ≤ v.
Assume Hv3: x < v * v.
Apply L1R w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: 0 ≤ w.
Assume Hw3: x < w * w.
We prove the intermediate claim L21: ∃k, nat_p k ∧ v ∈ R_ k ∧ w ∈ R_ k.
Apply famunionE ω R_ v Hv to the current goal.
Let k' be given.
Assume H.
Apply H to the current goal.
Assume Hk'1: k' ∈ ω.
Assume Hk'2: v ∈ R_ k'.
Apply famunionE ω R_ w Hw to the current goal.
Let k'' be given.
Assume H.
Apply H to the current goal.
Assume Hk''1: k'' ∈ ω.
Assume Hk''2: w ∈ R_ k''.
Apply ordinal_linear k' k'' (nat_p_ordinal k' (omega_nat_p k' Hk'1)) (nat_p_ordinal k'' (omega_nat_p k'' Hk''1)) to the current goal.
Assume H1: k' ⊆ k''.
We use k'' to witness the existential quantifier.
Apply and3I to the current goal.
An exact proof term for the current goal is omega_nat_p k'' Hk''1.
We will prove v ∈ R_ k''.
An exact proof term for the current goal is LR_mon k' k'' (omega_nat_p k' Hk'1) (omega_nat_p k'' Hk''1) H1 v Hk'2.
An exact proof term for the current goal is Hk''2.
Assume H1: k'' ⊆ k'.
We use k' to witness the existential quantifier.
Apply and3I to the current goal.
An exact proof term for the current goal is omega_nat_p k' Hk'1.
An exact proof term for the current goal is Hk'2.
We will prove w ∈ R_ k'.
An exact proof term for the current goal is LR_mon k'' k' (omega_nat_p k'' Hk''1) (omega_nat_p k' Hk'1) H1 w Hk''2.
Apply L21 to the current goal.
Let k be given.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Assume Hk: nat_p k.
Assume Hvk: v ∈ R_ k.
Assume Hwk: w ∈ R_ k.
We prove the intermediate claim Lvwpos: 0 < v + w.
Apply SNoLeLt_tra 0 v (v + w) SNo_0 Hv1 (SNo_add_SNo v w Hv1 Hw1) Hv2 to the current goal.
We will prove v < v + w.
rewrite the current goal using add_SNo_0R v Hv1 (from right to left) at position 1.
We will prove v + 0 < v + w.
Apply add_SNo_Lt2 v 0 w Hv1 SNo_0 Hw1 to the current goal.
We will prove 0 < w.
Apply SNoLeLt_tra 0 y w SNo_0 H1 Hw1 Hynn to the current goal.
We will prove y < w.
Apply H4 to the current goal.
We will prove w ∈ R.
An exact proof term for the current goal is famunionI ω R_ k w (nat_p_omega k Hk) Hwk.
We prove the intermediate claim Lvw0: v + w ≠ 0.
Assume H.
Apply SNoLt_irref 0 to the current goal.
rewrite the current goal using H (from right to left) at position 2.
An exact proof term for the current goal is Lvwpos.
We prove the intermediate claim L22: (x + v * w) :/: (v + w) ∈ R_ (ordsucc k).
We will prove (x + v * w) :/: (v + w) ∈ SNo_sqrtaux x sqrt_SNo_nonneg (ordsucc k) 1.
rewrite the current goal using SNo_sqrtaux_S x 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 (x + v * w) :/: (v + w) ∈ R_ k ∪ SNo_sqrtauxset (L_ k) (L_ k) x ∪ SNo_sqrtauxset (R_ k) (R_ k) x.
Apply binunionI2 to the current goal.
An exact proof term for the current goal is SNo_sqrtauxset_I (R_ k) (R_ k) x v Hvk w Hwk Lvwpos.
We prove the intermediate claim L23: (x + v * w) :/: (v + w) ∈ R.
An exact proof term for the current goal is famunionI ω R_ (ordsucc k) ((x + v * w) :/: (v + w)) (nat_p_omega (ordsucc k) (nat_ordsucc k Hk)) L22.
We prove the intermediate claim L24: y < (x + v * w) :/: (v + w).
An exact proof term for the current goal is H4 ((x + v * w) :/: (v + w)) L23.
We prove the intermediate claim L25: v * y + y * w = y * (v + w).
Use transitivity with and y * v + y * w.
Use f_equal.
We will prove v * y = y * v.
An exact proof term for the current goal is mul_SNo_com v y Hv1 H1.
We will prove y * v + y * w = y * (v + w).
Use symmetry.
An exact proof term for the current goal is mul_SNo_distrL y v w H1 Hv1 Hw1.
We will prove False.
Apply SNoLt_irref (x + v * w) to the current goal.
Apply SNoLeLt_tra (x + v * w) (v * y + y * w) (x + v * w) (SNo_add_SNo x (v * w) Hx (SNo_mul_SNo v w Hv1 Hw1)) (SNo_add_SNo (v * y) (y * w) (SNo_mul_SNo v y Hv1 H1) (SNo_mul_SNo y w H1 Hw1)) (SNo_add_SNo x (v * w) Hx (SNo_mul_SNo v w Hv1 Hw1)) H10 to the current goal.
We will prove v * y + y * w < x + v * w.
rewrite the current goal using L25 (from left to right).
We will prove y * (v + w) < x + v * w.
rewrite the current goal using mul_div_SNo_invL (x + v * w) (v + w) (SNo_add_SNo x (v * w) Hx (SNo_mul_SNo v w Hv1 Hw1)) (SNo_add_SNo v w Hv1 Hw1) Lvw0 (from right to left).
We will prove y * (v + w) < ((x + v * w) :/: (v + w)) * (v + w).
An exact proof term for the current goal is pos_mul_SNo_Lt' y ((x + v * w) :/: (v + w)) (v + w) H1 (SNo_div_SNo (x + v * w) (v + w) (SNo_add_SNo x (v * w) Hx (SNo_mul_SNo v w Hv1 Hw1)) (SNo_add_SNo v w Hv1 Hw1)) (SNo_add_SNo v w Hv1 Hw1) Lvwpos L24.
Assume H7: SNoLev (y * y) ∈ SNoLev x.
We will prove False.
We prove the intermediate claim Lsryy: sqrt_SNo_nonneg (y * y) = y.
Apply IH (y * y) (SNoS_I2 (y * y) x Lyy Hx H7) Lyynn to the current goal.
Assume H.
Apply H to the current goal.
Assume H10: SNo (sqrt_SNo_nonneg (y * y)).
Assume H11: 0 ≤ sqrt_SNo_nonneg (y * y).
Assume H12: sqrt_SNo_nonneg (y * y) * sqrt_SNo_nonneg (y * y) = y * y.
An exact proof term for the current goal is SNo_nonneg_sqr_uniq (sqrt_SNo_nonneg (y * y)) y H10 H1 H11 Hynn H12.
Apply SNoLt_irref y to the current goal.
We will prove y < y.
rewrite the current goal using Lsryy (from right to left) at position 2.
We will prove y < sqrt_SNo_nonneg (y * y).
Apply H4 to the current goal.
We will prove sqrt_SNo_nonneg (y * y) ∈ R.
We prove the intermediate claim LyyR0: sqrt_SNo_nonneg (y * y) ∈ R_ 0.
We will prove sqrt_SNo_nonneg (y * y) ∈ SNo_sqrtaux x sqrt_SNo_nonneg 0 1.
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 (y * y) ∈ {sqrt_SNo_nonneg w|w ∈ SNoR x}.
Apply ReplI to the current goal.
We will prove y * y ∈ SNoR x.
An exact proof term for the current goal is SNoR_I x Hx (y * y) Lyy H7 H6.
An exact proof term for the current goal is famunionI ω R_ 0 (sqrt_SNo_nonneg (y * y)) (nat_p_omega 0 nat_0) LyyR0.
∎