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: y * y < x.
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 (y * y) x Lyy Hx H6 to the current goal.
Let u be given.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev (y * y) ∩ SNoLev x.
Assume Hu3: SNoEq_ (SNoLev u) u (y * y).
Assume Hu4: SNoEq_ (SNoLev u) u x.
Assume Hu5: y * y < u.
Assume Hu6: u < x.
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 (y * y) u SNo_0 Lyy Hu1 Lyynn 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 binintersectE2 (SNoLev (y * y)) (SNoLev x) (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 Lsruy: sqrt_SNo_nonneg u ≤ y.
Apply SNoLtLe to the current goal.
We will prove sqrt_SNo_nonneg u < y.
Apply H3 to the current goal.
We will prove sqrt_SNo_nonneg u ∈ L.
We prove the intermediate claim Lsruy0: sqrt_SNo_nonneg u ∈ L_ 0.
We will prove sqrt_SNo_nonneg u ∈ 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 sqrt_SNo_nonneg u ∈ {sqrt_SNo_nonneg w|w ∈ SNoL_nonneg x}.
Apply ReplI to the current goal.
We will prove u ∈ {w ∈ SNoL x|0 ≤ w}.
Apply SepI to the current goal.
Apply SNoL_I x Hx u Hu1 to the current goal.
An exact proof term for the current goal is binintersectE2 (SNoLev (y * y)) (SNoLev x) (SNoLev u) Hu2.
We will prove u < x.
An exact proof term for the current goal is Hu6.
An exact proof term for the current goal is Lunn.
An exact proof term for the current goal is famunionI ω L_ 0 (sqrt_SNo_nonneg u) (nat_p_omega 0 nat_0) Lsruy0.
We prove the intermediate claim Luyy: u ≤ y * y.
rewrite the current goal using H9 (from right to left).
We will prove sqrt_SNo_nonneg u * sqrt_SNo_nonneg u ≤ y * y.
An exact proof term for the current goal is nonneg_mul_SNo_Le2 (sqrt_SNo_nonneg u) (sqrt_SNo_nonneg u) y y H7 H7 H1 H1 H8 H8 Lsruy Lsruy.
Apply SNoLt_irref (y * y) to the current goal.
We will prove y * y < y * y.
An exact proof term for the current goal is SNoLtLe_tra (y * y) u (y * y) Lyy Hu1 Lyy Hu5 Luyy.
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 1.
We will prove sqrt_SNo_nonneg (y * y) < y.
Apply H3 to the current goal.
We will prove sqrt_SNo_nonneg (y * y) ∈ ⋃k ∈ ωL_ k.
We prove the intermediate claim LyyL0: sqrt_SNo_nonneg (y * y) ∈ L_ 0.
We will prove sqrt_SNo_nonneg (y * y) ∈ 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 sqrt_SNo_nonneg (y * y) ∈ {sqrt_SNo_nonneg w|w ∈ SNoL_nonneg x}.
Apply ReplI to the current goal.
We will prove y * y ∈ SNoL_nonneg x.
We will prove y * y ∈ {w ∈ SNoL x|0 ≤ w}.
Apply SepI to the current goal.
An exact proof term for the current goal is SNoL_I x Hx (y * y) Lyy H7 H6.
We will prove 0 ≤ y * y.
An exact proof term for the current goal is Lyynn.
An exact proof term for the current goal is famunionI ω L_ 0 (sqrt_SNo_nonneg (y * y)) (nat_p_omega 0 nat_0) LyyL0.
Assume H7: SNoLev x ∈ SNoLev (y * y).
Assume H8: SNoEq_ (SNoLev x) (y * y) x.
Assume H9: SNoLev x ∉ y * y.
We prove the intermediate claim L3: x ∈ SNoR (y * y).
An exact proof term for the current goal is SNoR_I (y * y) Lyy x Hx H7 H6.
We prove the intermediate claim L4: ∀p : prop, (∀v ∈ L, ∀w ∈ R, v * y + y * w ≤ x + v * w → p) → p.
Let p be given.
Assume Hp.
Apply mul_SNo_SNoCut_SNoR_interpolate_impred L R L R HLR HLR y y (λq H ⇒ H) (λq H ⇒ H) x L3 to the current goal.
Let v be given.
Assume Hv: v ∈ L.
Let w be given.
Assume Hw: w ∈ R.
Assume H10: v * y + y * w ≤ x + v * w.
An exact proof term for the current goal is Hp v Hv w Hw H10.
Let v be given.
Assume Hv: v ∈ R.
Let w be given.
Assume Hw: w ∈ L.
Assume H10: v * y + y * w ≤ x + v * w.
Apply Hp w Hw v Hv to the current goal.
We will prove w * y + y * v ≤ x + w * v.
We prove the intermediate claim Lv1: SNo v.
An exact proof term for the current goal is HR v Hv.
We prove the intermediate claim Lw1: SNo w.
An exact proof term for the current goal is HL w Hw.
rewrite the current goal using mul_SNo_com w v Lw1 Lv1 (from left to right).
We will prove w * y + y * v ≤ x + v * w.
Apply mul_SNo_com w y Lw1 H1 (λ_ u ⇒ u + y * v ≤ x + v * w) to the current goal.
We will prove y * w + y * v ≤ x + v * w.
Apply mul_SNo_com y v H1 Lv1 (λ_ u ⇒ y * w + u ≤ x + v * w) to the current goal.
We will prove y * w + v * y ≤ x + v * w.
Apply add_SNo_com (y * w) (v * y) (SNo_mul_SNo y w H1 Lw1) (SNo_mul_SNo v y Lv1 H1) (λ_ u ⇒ u ≤ x + v * w) to the current goal.
An exact proof term for the current goal is H10.
Apply L4 to the current goal.
Let v be given.
Assume Hv: v ∈ L.
Let w be given.
Assume Hw: w ∈ R.
Assume H10: v * y + y * w ≤ x + v * w.
Apply L1L v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: 0 ≤ v.
Assume Hv3: v * v < x.
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 L5: ∃k, nat_p k ∧ v ∈ L_ k ∧ w ∈ R_ 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 ω 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 ∈ 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 ∈ 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 L5 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 ∈ 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 L6: (x + v * w) :/: (v + w) ∈ L_ (ordsucc k).
We will prove (x + v * w) :/: (v + w) ∈ SNo_sqrtaux x sqrt_SNo_nonneg (ordsucc k) 0.
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_0_eq (from left to right).
We will prove (x + v * w) :/: (v + w) ∈ L_ k ∪ SNo_sqrtauxset (L_ k) (R_ k) x.
Apply binunionI2 to the current goal.
An exact proof term for the current goal is SNo_sqrtauxset_I (L_ k) (R_ k) x v Hvk w Hwk Lvwpos.
We prove the intermediate claim L7: (x + v * w) :/: (v + w) ∈ L.
An exact proof term for the current goal is famunionI ω L_ (ordsucc k) ((x + v * w) :/: (v + w)) (nat_p_omega (ordsucc k) (nat_ordsucc k Hk)) L6.
We prove the intermediate claim L8: (x + v * w) :/: (v + w) < y.
An exact proof term for the current goal is H3 ((x + v * w) :/: (v + w)) L7.
We prove the intermediate claim L9: 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 (v * y + y * w) to the current goal.
Apply SNoLeLt_tra (v * y + y * w) (x + v * w) (v * y + y * w) (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)) (SNo_add_SNo (v * y) (y * w) (SNo_mul_SNo v y Hv1 H1) (SNo_mul_SNo y w H1 Hw1)) H10 to the current goal.
We will prove x + v * w < v * y + y * w.
rewrite the current goal using L9 (from left to right).
We will prove x + v * w < y * (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 ((x + v * w) :/: (v + w)) * (v + w) < y * (v + w).
An exact proof term for the current goal is pos_mul_SNo_Lt' ((x + v * w) :/: (v + w)) y (v + w) (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)) H1 (SNo_add_SNo v w Hv1 Hw1) Lvwpos L8.
∎