Let x be given.
Assume Hx Hxnonneg IH.
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.
Apply nat_ind to the current goal.
We will prove (∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg 0 0, SNo y ∧ 0 ≤ y ∧ y * y < x) ∧ (∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg 0 1, SNo y ∧ 0 ≤ y ∧ x < y * y).
rewrite the current goal using SNo_sqrtaux_0 x sqrt_SNo_nonneg (from left to right).
Apply andI to the current goal.
Let y be given.
rewrite the current goal using tuple_2_0_eq (from left to right).
Assume Hy: y ∈ {sqrt_SNo_nonneg w|w ∈ SNoL_nonneg x}.
We will prove SNo y ∧ 0 ≤ y ∧ y * y < x.
Apply ReplE_impred (SNoL_nonneg x) sqrt_SNo_nonneg y Hy to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL_nonneg x.
Assume Hyw: y = sqrt_SNo_nonneg w.
Apply SepE (SNoL x) (λw ⇒ 0 ≤ w) w Hw to the current goal.
Assume Hw: w ∈ SNoL x.
Assume Hwnonneg: 0 ≤ w.
Apply SNoL_E x Hx w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
We prove the intermediate claim Lw: w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 w x Hw1 Hx Hw2.
Apply IH w Lw Hwnonneg to the current goal.
Assume H.
Apply H to the current goal.
Assume IHa: SNo (sqrt_SNo_nonneg w).
Assume IHb: 0 ≤ sqrt_SNo_nonneg w.
Assume IHc: sqrt_SNo_nonneg w * sqrt_SNo_nonneg w = w.
Apply and3I to the current goal.
rewrite the current goal using Hyw (from left to right).
An exact proof term for the current goal is IHa.
rewrite the current goal using Hyw (from left to right).
An exact proof term for the current goal is IHb.
rewrite the current goal using Hyw (from left to right).
We will prove sqrt_SNo_nonneg w * sqrt_SNo_nonneg w < x.
rewrite the current goal using IHc (from left to right).
An exact proof term for the current goal is Hw3.
Let y be given.
rewrite the current goal using tuple_2_1_eq (from left to right).
Assume Hy: y ∈ {sqrt_SNo_nonneg z|z ∈ SNoR x}.
We will prove SNo y ∧ 0 ≤ y ∧ x < y * y.
Apply ReplE_impred (SNoR x) sqrt_SNo_nonneg y Hy to the current goal.
Let z be given.
Assume Hz: z ∈ SNoR x.
Assume Hyz: y = sqrt_SNo_nonneg z.
Apply SNoR_E x Hx z Hz to the current goal.
Assume Hz1 Hz2 Hz3.
We prove the intermediate claim Lz: z ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 z x Hz1 Hx Hz2.
We prove the intermediate claim Lznonneg: 0 ≤ z.
An exact proof term for the current goal is SNoLe_tra 0 x z SNo_0 Hx Hz1 Hxnonneg (SNoLtLe x z Hz3).
Apply IH z Lz Lznonneg to the current goal.
Assume H.
Apply H to the current goal.
Assume IHa: SNo (sqrt_SNo_nonneg z).
Assume IHb: 0 ≤ sqrt_SNo_nonneg z.
Assume IHc: sqrt_SNo_nonneg z * sqrt_SNo_nonneg z = z.
Apply and3I to the current goal.
rewrite the current goal using Hyz (from left to right).
An exact proof term for the current goal is IHa.
rewrite the current goal using Hyz (from left to right).
An exact proof term for the current goal is IHb.
rewrite the current goal using Hyz (from left to right).
We will prove x < sqrt_SNo_nonneg z * sqrt_SNo_nonneg z.
rewrite the current goal using IHc (from left to right).
An exact proof term for the current goal is Hz3.
Let k be given.
Assume Hk: nat_p k.
Assume IHk: (∀y ∈ L_ k, SNo y ∧ 0 ≤ y ∧ y * y < x) ∧ (∀y ∈ R_ k, SNo y ∧ 0 ≤ y ∧ x < y * y).
Apply IHk to the current goal.
Assume IHk0 IHk1.
We will prove (∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg (ordsucc k) 0, SNo y ∧ 0 ≤ y ∧ y * y < x) ∧ (∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg (ordsucc k) 1, SNo y ∧ 0 ≤ y ∧ x < y * y).
rewrite the current goal using SNo_sqrtaux_S x sqrt_SNo_nonneg k Hk (from left to right).
Apply andI to the current goal.
Let y be given.
rewrite the current goal using tuple_2_0_eq (from left to right).
Apply binunionE' to the current goal.
An exact proof term for the current goal is IHk0 y.
Assume Hy: y ∈ SNo_sqrtauxset (L_ k) (R_ k) x.
Apply SNo_sqrtauxset_E (L_ k) (R_ k) x y Hy to the current goal.
Let w be given.
Assume Hw: w ∈ L_ k.
Let z be given.
Assume Hz: z ∈ R_ k.
Assume Hwpzpos: 0 < w + z.
Assume Hywz: y = (x + w * z) :/: (w + z).
Apply IHk0 w Hw to the current goal.
Assume H.
Apply H to the current goal.
Assume Hw1: SNo w.
Assume Hw2: 0 ≤ w.
Assume Hw3: w * w < x.
Apply IHk1 z Hz to the current goal.
Assume H.
Apply H to the current goal.
Assume Hz1: SNo z.
Assume Hz2: 0 ≤ z.
Assume Hz3: x < z * z.
We will prove SNo y ∧ 0 ≤ y ∧ y * y < x.
We prove the intermediate claim Lwz: SNo (w * z).
An exact proof term for the current goal is SNo_mul_SNo w z Hw1 Hz1.
We prove the intermediate claim Lxpwz: SNo (x + w * z).
An exact proof term for the current goal is SNo_add_SNo x (w * z) Hx Lwz.
We prove the intermediate claim Lwpz: SNo (w + z).
An exact proof term for the current goal is SNo_add_SNo w z Hw1 Hz1.
We prove the intermediate claim Ly: SNo y.
rewrite the current goal using Hywz (from left to right).
An exact proof term for the current goal is SNo_div_SNo (x + w * z) (w + z) Lxpwz Lwpz.
We prove the intermediate claim Lxpwznonneg: 0 ≤ x + w * z.
rewrite the current goal using add_SNo_0L 0 SNo_0 (from right to left).
Apply add_SNo_Le3 0 0 x (w * z) SNo_0 SNo_0 Hx Lwz Hxnonneg to the current goal.
We will prove 0 ≤ w * z.
An exact proof term for the current goal is mul_SNo_nonneg_nonneg w z Hw1 Hz1 Hw2 Hz2.
We prove the intermediate claim Lynonneg: 0 ≤ y.
We will prove 0 ≤ y.
rewrite the current goal using Hywz (from left to right).
We will prove 0 ≤ (x + w * z) :/: (w + z).
Apply SNoLeE 0 (x + w * z) SNo_0 Lxpwz Lxpwznonneg to the current goal.
Assume H1: 0 < x + w * z.
Apply SNoLtLe to the current goal.
Apply div_SNo_pos_pos (x + w * z) (w + z) Lxpwz Lwpz to the current goal.
We will prove 0 < x + w * z.
An exact proof term for the current goal is H1.
We will prove 0 < w + z.
An exact proof term for the current goal is Hwpzpos.
Assume H1: 0 = x + w * z.
rewrite the current goal using H1 (from right to left).
We will prove 0 ≤ 0 :/: (w + z).
rewrite the current goal using div_SNo_0_num (w + z) Lwpz (from left to right).
Apply SNoLe_ref to the current goal.
Apply and3I to the current goal.
An exact proof term for the current goal is Ly.
An exact proof term for the current goal is Lynonneg.
We will prove y * y < x.
rewrite the current goal using Hywz (from left to right).
We will prove ((x + w * z) :/: (w + z)) * ((x + w * z) :/: (w + z)) < x.
rewrite the current goal using mul_div_SNo_both (x + w * z) (w + z) (x + w * z) (w + z) Lxpwz Lwpz Lxpwz Lwpz (from left to right).
We will prove ((x + w * z) * (x + w * z)) :/: ((w + z) * (w + z)) < x.
Apply div_SNo_pos_LtL ((x + w * z) * (x + w * z)) ((w + z) * (w + z)) x (SNo_mul_SNo (x + w * z) (x + w * z) Lxpwz Lxpwz) (SNo_mul_SNo (w + z) (w + z) Lwpz Lwpz) Hx to the current goal.
We will prove 0 < (w + z) * (w + z).
An exact proof term for the current goal is mul_SNo_pos_pos (w + z) (w + z) Lwpz Lwpz Hwpzpos Hwpzpos.
We will prove ((x + w * z) * (x + w * z)) < x * ((w + z) * (w + z)).
rewrite the current goal using SNo_foil x (w * z) x (w * z) Hx Lwz (from left to right).
rewrite the current goal using SNo_foil w z w z Hw1 Hz1 Hw1 Hz1 (from left to right).
We will prove x * x + x * w * z + (w * z) * x + (w * z) * w * z < x * (w * w + w * z + z * w + z * z).
rewrite the current goal using mul_SNo_com z w Hz1 Hw1 (from left to right).
rewrite the current goal using add_SNo_rotate_4_1 (w * z) (w * z) (z * z) (w * w) Lwz Lwz (SNo_mul_SNo z z Hz1 Hz1) (SNo_mul_SNo w w Hw1 Hw1) (from right to left).
We will prove x * x + x * w * z + (w * z) * x + (w * z) * w * z < x * (w * z + w * z + z * z + w * w).
rewrite the current goal using mul_SNo_com (w * z) x Lwz Hx (from left to right).
We will prove x * x + x * w * z + x * w * z + (w * z) * w * z < x * (w * z + w * z + z * z + w * w).
We prove the intermediate claim Lxwz: SNo (x * w * z).
An exact proof term for the current goal is SNo_mul_SNo x (w * z) Hx Lwz.
rewrite the current goal using add_SNo_rotate_4_1 (x * w * z) (x * w * z) ((w * z) * w * z) (x * x) Lxwz Lxwz (SNo_mul_SNo (w * z) (w * z) Lwz Lwz) (SNo_mul_SNo x x Hx Hx) (from right to left).
We will prove x * w * z + x * w * z + (w * z) * w * z + x * x < x * (w * z + w * z + z * z + w * w).
rewrite the current goal using mul_SNo_distrL x (w * z) (w * z + z * z + w * w) Hx Lwz (SNo_add_SNo_3 (w * z) (z * z) (w * w) Lwz (SNo_mul_SNo z z Hz1 Hz1) (SNo_mul_SNo w w Hw1 Hw1)) (from left to right).
We will prove x * w * z + x * w * z + (w * z) * w * z + x * x < x * w * z + x * (w * z + z * z + w * w).
rewrite the current goal using mul_SNo_distrL x (w * z) (z * z + w * w) Hx Lwz (SNo_add_SNo (z * z) (w * w) (SNo_mul_SNo z z Hz1 Hz1) (SNo_mul_SNo w w Hw1 Hw1)) (from left to right).
We will prove x * w * z + x * w * z + (w * z) * w * z + x * x < x * w * z + x * w * z + x * (z * z + w * w).
We prove the intermediate claim Lxwz: SNo (x * w * z).
An exact proof term for the current goal is SNo_mul_SNo_3 x w z Hx Hw1 Hz1.
Apply add_SNo_Lt2 (x * w * z) (x * w * z + (w * z) * w * z + x * x) (x * w * z + x * (z * z + w * w)) Lxwz (SNo_add_SNo_3 (x * w * z) ((w * z) * w * z) (x * x) Lxwz (SNo_mul_SNo (w * z) (w * z) Lwz Lwz) (SNo_mul_SNo x x Hx Hx)) (SNo_add_SNo (x * w * z) (x * (z * z + w * w)) Lxwz (SNo_mul_SNo x (z * z + w * w) Hx (SNo_add_SNo (z * z) (w * w) (SNo_mul_SNo z z Hz1 Hz1) (SNo_mul_SNo w w Hw1 Hw1)))) to the current goal.
We will prove x * w * z + (w * z) * w * z + x * x < x * w * z + x * (z * z + w * w).
Apply add_SNo_Lt2 (x * w * z) ((w * z) * w * z + x * x) (x * (z * z + w * w)) Lxwz (SNo_add_SNo ((w * z) * w * z) (x * x) (SNo_mul_SNo (w * z) (w * z) Lwz Lwz) (SNo_mul_SNo x x Hx Hx)) (SNo_mul_SNo x (z * z + w * w) Hx (SNo_add_SNo (z * z) (w * w) (SNo_mul_SNo z z Hz1 Hz1) (SNo_mul_SNo w w Hw1 Hw1))) to the current goal.
We will prove (w * z) * w * z + x * x < x * (z * z + w * w).
rewrite the current goal using mul_SNo_distrL x (z * z) (w * w) Hx (SNo_mul_SNo z z Hz1 Hz1) (SNo_mul_SNo w w Hw1 Hw1) (from left to right).
We will prove (w * z) * w * z + x * x < x * z * z + x * w * w.
rewrite the current goal using mul_SNo_com x (w * w) Hx (SNo_mul_SNo w w Hw1 Hw1) (from left to right).
We will prove (w * z) * w * z + x * x < x * z * z + (w * w) * x.
rewrite the current goal using add_SNo_0L ((w * z) * w * z + x * x) (SNo_add_SNo ((w * z) * w * z) (x * x) (SNo_mul_SNo (w * z) (w * z) Lwz Lwz) (SNo_mul_SNo x x Hx Hx)) (from right to left).
We will prove 0 + (w * z) * w * z + x * x < x * z * z + (w * w) * x.
Apply add_SNo_minus_Lt2 (x * z * z + (w * w) * x) ((w * z) * w * z + x * x) 0 (SNo_add_SNo (x * z * z) ((w * w) * x) (SNo_mul_SNo x (z * z) Hx (SNo_mul_SNo z z Hz1 Hz1)) (SNo_mul_SNo (w * w) x (SNo_mul_SNo w w Hw1 Hw1) Hx)) (SNo_add_SNo ((w * z) * w * z) (x * x) (SNo_mul_SNo (w * z) (w * z) Lwz Lwz) (SNo_mul_SNo x x Hx Hx)) SNo_0 to the current goal.
We will prove 0 < (x * z * z + (w * w) * x) + - ((w * z) * w * z + x * x).
rewrite the current goal using add_SNo_assoc (x * z * z) ((w * w) * x) (- ((w * z) * w * z + x * x)) (SNo_mul_SNo x (z * z) Hx (SNo_mul_SNo z z Hz1 Hz1)) (SNo_mul_SNo (w * w) x (SNo_mul_SNo w w Hw1 Hw1) Hx) (SNo_minus_SNo ((w * z) * w * z + x * x) (SNo_add_SNo ((w * z) * w * z) (x * x) (SNo_mul_SNo (w * z) (w * z) Lwz Lwz) (SNo_mul_SNo x x Hx Hx))) (from right to left).
rewrite the current goal using minus_add_SNo_distr ((w * z) * w * z) (x * x) (SNo_mul_SNo (w * z) (w * z) Lwz Lwz) (SNo_mul_SNo x x Hx Hx) (from left to right).
We will prove 0 < x * z * z + (w * w) * x + - (w * z) * w * z + - x * x.
rewrite the current goal using add_SNo_rotate_3_1 ((w * w) * x) (- (w * z) * w * z) (- x * x) (SNo_mul_SNo (w * w) x (SNo_mul_SNo w w Hw1 Hw1) Hx) (SNo_minus_SNo ((w * z) * w * z) (SNo_mul_SNo (w * z) (w * z) Lwz Lwz)) (SNo_minus_SNo (x * x) (SNo_mul_SNo x x Hx Hx)) (from left to right).
We will prove 0 < x * z * z + - x * x + (w * w) * x + - (w * z) * w * z.
rewrite the current goal using add_SNo_com ((w * w) * x) (- (w * z) * w * z) (SNo_mul_SNo (w * w) x (SNo_mul_SNo w w Hw1 Hw1) Hx) (SNo_minus_SNo ((w * z) * w * z) (SNo_mul_SNo (w * z) (w * z) Lwz Lwz)) (from left to right).
We will prove 0 < x * z * z + - x * x + - (w * z) * w * z + (w * w) * x.
rewrite the current goal using mul_SNo_assoc w z (w * z) Hw1 Hz1 Lwz (from right to left).
We will prove 0 < x * z * z + - x * x + - w * z * w * z + (w * w) * x.
rewrite the current goal using mul_SNo_com_3_0_1 z w z Hz1 Hw1 Hz1 (from left to right).
We will prove 0 < x * z * z + - x * x + - w * w * z * z + (w * w) * x.
rewrite the current goal using mul_SNo_assoc w w (z * z) Hw1 Hw1 (SNo_mul_SNo z z Hz1 Hz1) (from left to right).
rewrite the current goal using SNo_foil_mm x (w * w) (z * z) x Hx (SNo_mul_SNo w w Hw1 Hw1) (SNo_mul_SNo z z Hz1 Hz1) Hx (from right to left).
We will prove 0 < (x + - w * w) * (z * z + - x).
Apply mul_SNo_pos_pos (x + - w * w) (z * z + - x) (SNo_add_SNo x (- w * w) Hx (SNo_minus_SNo (w * w) (SNo_mul_SNo w w Hw1 Hw1))) (SNo_add_SNo (z * z) (- x) (SNo_mul_SNo z z Hz1 Hz1) (SNo_minus_SNo x Hx)) to the current goal.
We will prove 0 < x + - w * w.
An exact proof term for the current goal is SNoLt_minus_pos (w * w) x (SNo_mul_SNo w w Hw1 Hw1) Hx Hw3.
We will prove 0 < z * z + - x.
An exact proof term for the current goal is SNoLt_minus_pos x (z * z) Hx (SNo_mul_SNo z z Hz1 Hz1) Hz3.
An exact proof term for the current goal is Hx.
We will prove SNo (w * z).
An exact proof term for the current goal is Lwz.
Let y be given.
rewrite the current goal using tuple_2_1_eq (from left to right).
Apply binunionE' to the current goal.
Apply binunionE' to the current goal.
An exact proof term for the current goal is IHk1 y.
Assume Hy: y ∈ SNo_sqrtauxset (L_ k) (L_ k) x.
We will prove SNo y ∧ 0 ≤ y ∧ x < y * y.
Apply SNo_sqrtauxset_E (L_ k) (L_ k) x y Hy to the current goal.
Let w be given.
Assume Hw: w ∈ L_ k.
Let w' be given.
Assume Hw': w' ∈ L_ k.
Assume Hww'pos: 0 < w + w'.
Assume Hyww': y = (x + w * w') :/: (w + w').
Apply IHk0 w Hw to the current goal.
Assume H.
Apply H to the current goal.
Assume Hw1: SNo w.
Assume Hw2: 0 ≤ w.
Assume Hw3: w * w < x.
Apply IHk0 w' Hw' to the current goal.
Assume H.
Apply H to the current goal.
Assume Hw'1: SNo w'.
Assume Hw'2: 0 ≤ w'.
Assume Hw'3: w' * w' < x.
We will prove SNo y ∧ 0 ≤ y ∧ x < y * y.
We prove the intermediate claim Lww': SNo (w * w').
An exact proof term for the current goal is SNo_mul_SNo w w' Hw1 Hw'1.
We prove the intermediate claim Lxpww': SNo (x + w * w').
An exact proof term for the current goal is SNo_add_SNo x (w * w') Hx Lww'.
We prove the intermediate claim Lwpw': SNo (w + w').
An exact proof term for the current goal is SNo_add_SNo w w' Hw1 Hw'1.
We prove the intermediate claim Ly: SNo y.
rewrite the current goal using Hyww' (from left to right).
An exact proof term for the current goal is SNo_div_SNo (x + w * w') (w + w') Lxpww' Lwpw'.
We prove the intermediate claim Lxpww'nonneg: 0 ≤ x + w * w'.
rewrite the current goal using add_SNo_0L 0 SNo_0 (from right to left).
Apply add_SNo_Le3 0 0 x (w * w') SNo_0 SNo_0 Hx Lww' Hxnonneg to the current goal.
We will prove 0 ≤ w * w'.
An exact proof term for the current goal is mul_SNo_nonneg_nonneg w w' Hw1 Hw'1 Hw2 Hw'2.
We prove the intermediate claim Lynonneg: 0 ≤ y.
We will prove 0 ≤ y.
rewrite the current goal using Hyww' (from left to right).
We will prove 0 ≤ (x + w * w') :/: (w + w').
Apply SNoLeE 0 (x + w * w') SNo_0 Lxpww' Lxpww'nonneg to the current goal.
Assume H1: 0 < x + w * w'.
Apply SNoLtLe to the current goal.
Apply div_SNo_pos_pos (x + w * w') (w + w') Lxpww' Lwpw' to the current goal.
We will prove 0 < x + w * w'.
An exact proof term for the current goal is H1.
We will prove 0 < w + w'.
An exact proof term for the current goal is Hww'pos.
Assume H1: 0 = x + w * w'.
rewrite the current goal using H1 (from right to left).
We will prove 0 ≤ 0 :/: (w + w').
rewrite the current goal using div_SNo_0_num (w + w') Lwpw' (from left to right).
Apply SNoLe_ref to the current goal.
Apply and3I to the current goal.
An exact proof term for the current goal is Ly.
An exact proof term for the current goal is Lynonneg.
We will prove x < y * y.
rewrite the current goal using Hyww' (from left to right).
We will prove x < ((x + w * w') :/: (w + w')) * ((x + w * w') :/: (w + w')).
rewrite the current goal using mul_div_SNo_both (x + w * w') (w + w') (x + w * w') (w + w') Lxpww' Lwpw' Lxpww' Lwpw' (from left to right).
We will prove x < ((x + w * w') * (x + w * w')) :/: ((w + w') * (w + w')).
Apply div_SNo_pos_LtR ((x + w * w') * (x + w * w')) ((w + w') * (w + w')) x (SNo_mul_SNo (x + w * w') (x + w * w') Lxpww' Lxpww') (SNo_mul_SNo (w + w') (w + w') Lwpw' Lwpw') Hx to the current goal.
We will prove 0 < (w + w') * (w + w').
An exact proof term for the current goal is mul_SNo_pos_pos (w + w') (w + w') Lwpw' Lwpw' Hww'pos Hww'pos.
We will prove x * ((w + w') * (w + w')) < ((x + w * w') * (x + w * w')).
rewrite the current goal using SNo_foil x (w * w') x (w * w') Hx Lww' (from left to right).
rewrite the current goal using SNo_foil w w' w w' Hw1 Hw'1 Hw1 Hw'1 (from left to right).
We will prove x * (w * w + w * w' + w' * w + w' * w') < x * x + x * w * w' + (w * w') * x + (w * w') * w * w'.
rewrite the current goal using mul_SNo_com w' w Hw'1 Hw1 (from left to right).
rewrite the current goal using add_SNo_rotate_4_1 (w * w') (w * w') (w' * w') (w * w) Lww' Lww' (SNo_mul_SNo w' w' Hw'1 Hw'1) (SNo_mul_SNo w w Hw1 Hw1) (from right to left).
We will prove x * (w * w' + w * w' + w' * w' + w * w) < x * x + x * w * w' + (w * w') * x + (w * w') * w * w'.
rewrite the current goal using mul_SNo_com (w * w') x Lww' Hx (from left to right).
We will prove x * (w * w' + w * w' + w' * w' + w * w) < x * x + x * w * w' + x * w * w' + (w * w') * w * w'.
We prove the intermediate claim Lxww': SNo (x * w * w').
An exact proof term for the current goal is SNo_mul_SNo x (w * w') Hx Lww'.
rewrite the current goal using add_SNo_rotate_4_1 (x * w * w') (x * w * w') ((w * w') * w * w') (x * x) Lxww' Lxww' (SNo_mul_SNo (w * w') (w * w') Lww' Lww') (SNo_mul_SNo x x Hx Hx) (from right to left).
We will prove x * (w * w' + w * w' + w' * w' + w * w) < x * w * w' + x * w * w' + (w * w') * w * w' + x * x.
rewrite the current goal using mul_SNo_distrL x (w * w') (w * w' + w' * w' + w * w) Hx Lww' (SNo_add_SNo_3 (w * w') (w' * w') (w * w) Lww' (SNo_mul_SNo w' w' Hw'1 Hw'1) (SNo_mul_SNo w w Hw1 Hw1)) (from left to right).
We will prove x * w * w' + x * (w * w' + w' * w' + w * w) < x * w * w' + x * w * w' + (w * w') * w * w' + x * x.
rewrite the current goal using mul_SNo_distrL x (w * w') (w' * w' + w * w) Hx Lww' (SNo_add_SNo (w' * w') (w * w) (SNo_mul_SNo w' w' Hw'1 Hw'1) (SNo_mul_SNo w w Hw1 Hw1)) (from left to right).
We will prove x * w * w' + x * w * w' + x * (w' * w' + w * w) < x * w * w' + x * w * w' + (w * w') * w * w' + x * x.
We prove the intermediate claim Lxww': SNo (x * w * w').
An exact proof term for the current goal is SNo_mul_SNo_3 x w w' Hx Hw1 Hw'1.
Apply add_SNo_Lt2 (x * w * w') (x * w * w' + x * (w' * w' + w * w)) (x * w * w' + (w * w') * w * w' + x * x) Lxww' (SNo_add_SNo (x * w * w') (x * (w' * w' + w * w)) Lxww' (SNo_mul_SNo x (w' * w' + w * w) Hx (SNo_add_SNo (w' * w') (w * w) (SNo_mul_SNo w' w' Hw'1 Hw'1) (SNo_mul_SNo w w Hw1 Hw1)))) (SNo_add_SNo_3 (x * w * w') ((w * w') * w * w') (x * x) Lxww' (SNo_mul_SNo (w * w') (w * w') Lww' Lww') (SNo_mul_SNo x x Hx Hx)) to the current goal.
We will prove x * w * w' + x * (w' * w' + w * w) < x * w * w' + (w * w') * w * w' + x * x.
Apply add_SNo_Lt2 (x * w * w') (x * (w' * w' + w * w)) ((w * w') * w * w' + x * x) Lxww' (SNo_mul_SNo x (w' * w' + w * w) Hx (SNo_add_SNo (w' * w') (w * w) (SNo_mul_SNo w' w' Hw'1 Hw'1) (SNo_mul_SNo w w Hw1 Hw1))) (SNo_add_SNo ((w * w') * w * w') (x * x) (SNo_mul_SNo (w * w') (w * w') Lww' Lww') (SNo_mul_SNo x x Hx Hx)) to the current goal.
We will prove x * (w' * w' + w * w) < (w * w') * w * w' + x * x.
rewrite the current goal using mul_SNo_distrL x (w' * w') (w * w) Hx (SNo_mul_SNo w' w' Hw'1 Hw'1) (SNo_mul_SNo w w Hw1 Hw1) (from left to right).
We will prove x * w' * w' + x * w * w < (w * w') * w * w' + x * x.
rewrite the current goal using mul_SNo_com x (w * w) Hx (SNo_mul_SNo w w Hw1 Hw1) (from left to right).
We will prove x * w' * w' + (w * w) * x < (w * w') * w * w' + x * x.
rewrite the current goal using add_SNo_0L ((w * w') * w * w' + x * x) (SNo_add_SNo ((w * w') * w * w') (x * x) (SNo_mul_SNo (w * w') (w * w') Lww' Lww') (SNo_mul_SNo x x Hx Hx)) (from right to left).
We will prove x * w' * w' + (w * w) * x < 0 + (w * w') * w * w' + x * x.
Apply add_SNo_minus_Lt1 (x * w' * w' + (w * w) * x) ((w * w') * w * w' + x * x) 0 (SNo_add_SNo (x * w' * w') ((w * w) * x) (SNo_mul_SNo x (w' * w') Hx (SNo_mul_SNo w' w' Hw'1 Hw'1)) (SNo_mul_SNo (w * w) x (SNo_mul_SNo w w Hw1 Hw1) Hx)) (SNo_add_SNo ((w * w') * w * w') (x * x) (SNo_mul_SNo (w * w') (w * w') Lww' Lww') (SNo_mul_SNo x x Hx Hx)) SNo_0 to the current goal.
We will prove (x * w' * w' + (w * w) * x) + - ((w * w') * w * w' + x * x) < 0.
rewrite the current goal using add_SNo_assoc (x * w' * w') ((w * w) * x) (- ((w * w') * w * w' + x * x)) (SNo_mul_SNo x (w' * w') Hx (SNo_mul_SNo w' w' Hw'1 Hw'1)) (SNo_mul_SNo (w * w) x (SNo_mul_SNo w w Hw1 Hw1) Hx) (SNo_minus_SNo ((w * w') * w * w' + x * x) (SNo_add_SNo ((w * w') * w * w') (x * x) (SNo_mul_SNo (w * w') (w * w') Lww' Lww') (SNo_mul_SNo x x Hx Hx))) (from right to left).
rewrite the current goal using minus_add_SNo_distr ((w * w') * w * w') (x * x) (SNo_mul_SNo (w * w') (w * w') Lww' Lww') (SNo_mul_SNo x x Hx Hx) (from left to right).
We will prove x * w' * w' + (w * w) * x + - (w * w') * w * w' + - x * x < 0.
rewrite the current goal using add_SNo_rotate_3_1 ((w * w) * x) (- (w * w') * w * w') (- x * x) (SNo_mul_SNo (w * w) x (SNo_mul_SNo w w Hw1 Hw1) Hx) (SNo_minus_SNo ((w * w') * w * w') (SNo_mul_SNo (w * w') (w * w') Lww' Lww')) (SNo_minus_SNo (x * x) (SNo_mul_SNo x x Hx Hx)) (from left to right).
We will prove x * w' * w' + - x * x + (w * w) * x + - (w * w') * w * w' < 0.
rewrite the current goal using add_SNo_com ((w * w) * x) (- (w * w') * w * w') (SNo_mul_SNo (w * w) x (SNo_mul_SNo w w Hw1 Hw1) Hx) (SNo_minus_SNo ((w * w') * w * w') (SNo_mul_SNo (w * w') (w * w') Lww' Lww')) (from left to right).
We will prove x * w' * w' + - x * x + - (w * w') * w * w' + (w * w) * x < 0.
rewrite the current goal using mul_SNo_assoc w w' (w * w') Hw1 Hw'1 Lww' (from right to left).
We will prove x * w' * w' + - x * x + - w * w' * w * w' + (w * w) * x < 0.
rewrite the current goal using mul_SNo_com_3_0_1 w' w w' Hw'1 Hw1 Hw'1 (from left to right).
We will prove x * w' * w' + - x * x + - w * w * w' * w' + (w * w) * x < 0.
rewrite the current goal using mul_SNo_assoc w w (w' * w') Hw1 Hw1 (SNo_mul_SNo w' w' Hw'1 Hw'1) (from left to right).
rewrite the current goal using SNo_foil_mm x (w * w) (w' * w') x Hx (SNo_mul_SNo w w Hw1 Hw1) (SNo_mul_SNo w' w' Hw'1 Hw'1) Hx (from right to left).
We will prove (x + - w * w) * (w' * w' + - x) < 0.
Apply mul_SNo_pos_neg (x + - w * w) (w' * w' + - x) (SNo_add_SNo x (- w * w) Hx (SNo_minus_SNo (w * w) (SNo_mul_SNo w w Hw1 Hw1))) (SNo_add_SNo (w' * w') (- x) (SNo_mul_SNo w' w' Hw'1 Hw'1) (SNo_minus_SNo x Hx)) to the current goal.
We will prove 0 < x + - w * w.
An exact proof term for the current goal is SNoLt_minus_pos (w * w) x (SNo_mul_SNo w w Hw1 Hw1) Hx Hw3.
We will prove w' * w' + - x < 0.
Apply add_SNo_minus_Lt1b (w' * w') x 0 (SNo_mul_SNo w' w' Hw'1 Hw'1) Hx SNo_0 to the current goal.
We will prove w' * w' < 0 + x.
rewrite the current goal using add_SNo_0L x Hx (from left to right).
We will prove w' * w' < x.
An exact proof term for the current goal is Hw'3.
An exact proof term for the current goal is Hx.
We will prove SNo (w * w').
An exact proof term for the current goal is Lww'.
Assume Hy: y ∈ SNo_sqrtauxset (R_ k) (R_ k) x.
We will prove SNo y ∧ 0 ≤ y ∧ x < y * y.
Apply SNo_sqrtauxset_E (R_ k) (R_ k) x y Hy to the current goal.
Let z be given.
Assume Hz: z ∈ R_ k.
Let z' be given.
Assume Hz': z' ∈ R_ k.
Assume Hzz'pos: 0 < z + z'.
Assume Hyzz': y = (x + z * z') :/: (z + z').
Apply IHk1 z Hz to the current goal.
Assume H.
Apply H to the current goal.
Assume Hz1: SNo z.
Assume Hz2: 0 ≤ z.
Assume Hz3: x < z * z.
Apply IHk1 z' Hz' to the current goal.
Assume H.
Apply H to the current goal.
Assume Hz'1: SNo z'.
Assume Hz'2: 0 ≤ z'.
Assume Hz'3: x < z' * z'.
We will prove SNo y ∧ 0 ≤ y ∧ x < y * y.
We prove the intermediate claim Lzz': SNo (z * z').
An exact proof term for the current goal is SNo_mul_SNo z z' Hz1 Hz'1.
We prove the intermediate claim Lxpzz': SNo (x + z * z').
An exact proof term for the current goal is SNo_add_SNo x (z * z') Hx Lzz'.
We prove the intermediate claim Lzpz': SNo (z + z').
An exact proof term for the current goal is SNo_add_SNo z z' Hz1 Hz'1.
We prove the intermediate claim Ly: SNo y.
rewrite the current goal using Hyzz' (from left to right).
An exact proof term for the current goal is SNo_div_SNo (x + z * z') (z + z') Lxpzz' Lzpz'.
We prove the intermediate claim Lxpzz'nonneg: 0 ≤ x + z * z'.
rewrite the current goal using add_SNo_0L 0 SNo_0 (from right to left).
Apply add_SNo_Le3 0 0 x (z * z') SNo_0 SNo_0 Hx Lzz' Hxnonneg to the current goal.
We will prove 0 ≤ z * z'.
An exact proof term for the current goal is mul_SNo_nonneg_nonneg z z' Hz1 Hz'1 Hz2 Hz'2.
We prove the intermediate claim Lynonneg: 0 ≤ y.
We will prove 0 ≤ y.
rewrite the current goal using Hyzz' (from left to right).
We will prove 0 ≤ (x + z * z') :/: (z + z').
Apply SNoLeE 0 (x + z * z') SNo_0 Lxpzz' Lxpzz'nonneg to the current goal.
Assume H1: 0 < x + z * z'.
Apply SNoLtLe to the current goal.
Apply div_SNo_pos_pos (x + z * z') (z + z') Lxpzz' Lzpz' to the current goal.
We will prove 0 < x + z * z'.
An exact proof term for the current goal is H1.
We will prove 0 < z + z'.
An exact proof term for the current goal is Hzz'pos.
Assume H1: 0 = x + z * z'.
rewrite the current goal using H1 (from right to left).
We will prove 0 ≤ 0 :/: (z + z').
rewrite the current goal using div_SNo_0_num (z + z') Lzpz' (from left to right).
Apply SNoLe_ref to the current goal.
Apply and3I to the current goal.
An exact proof term for the current goal is Ly.
An exact proof term for the current goal is Lynonneg.
We will prove x < y * y.
rewrite the current goal using Hyzz' (from left to right).
We will prove x < ((x + z * z') :/: (z + z')) * ((x + z * z') :/: (z + z')).
rewrite the current goal using mul_div_SNo_both (x + z * z') (z + z') (x + z * z') (z + z') Lxpzz' Lzpz' Lxpzz' Lzpz' (from left to right).
We will prove x < ((x + z * z') * (x + z * z')) :/: ((z + z') * (z + z')).
Apply div_SNo_pos_LtR ((x + z * z') * (x + z * z')) ((z + z') * (z + z')) x (SNo_mul_SNo (x + z * z') (x + z * z') Lxpzz' Lxpzz') (SNo_mul_SNo (z + z') (z + z') Lzpz' Lzpz') Hx to the current goal.
We will prove 0 < (z + z') * (z + z').
An exact proof term for the current goal is mul_SNo_pos_pos (z + z') (z + z') Lzpz' Lzpz' Hzz'pos Hzz'pos.
We will prove x * ((z + z') * (z + z')) < ((x + z * z') * (x + z * z')).
rewrite the current goal using SNo_foil x (z * z') x (z * z') Hx Lzz' (from left to right).
rewrite the current goal using SNo_foil z z' z z' Hz1 Hz'1 Hz1 Hz'1 (from left to right).
We will prove x * (z * z + z * z' + z' * z + z' * z') < x * x + x * z * z' + (z * z') * x + (z * z') * z * z'.
rewrite the current goal using mul_SNo_com z' z Hz'1 Hz1 (from left to right).
rewrite the current goal using add_SNo_rotate_4_1 (z * z') (z * z') (z' * z') (z * z) Lzz' Lzz' (SNo_mul_SNo z' z' Hz'1 Hz'1) (SNo_mul_SNo z z Hz1 Hz1) (from right to left).
We will prove x * (z * z' + z * z' + z' * z' + z * z) < x * x + x * z * z' + (z * z') * x + (z * z') * z * z'.
rewrite the current goal using mul_SNo_com (z * z') x Lzz' Hx (from left to right).
We will prove x * (z * z' + z * z' + z' * z' + z * z) < x * x + x * z * z' + x * z * z' + (z * z') * z * z'.
We prove the intermediate claim Lxzz': SNo (x * z * z').
An exact proof term for the current goal is SNo_mul_SNo x (z * z') Hx Lzz'.
rewrite the current goal using add_SNo_rotate_4_1 (x * z * z') (x * z * z') ((z * z') * z * z') (x * x) Lxzz' Lxzz' (SNo_mul_SNo (z * z') (z * z') Lzz' Lzz') (SNo_mul_SNo x x Hx Hx) (from right to left).
We will prove x * (z * z' + z * z' + z' * z' + z * z) < x * z * z' + x * z * z' + (z * z') * z * z' + x * x.
rewrite the current goal using mul_SNo_distrL x (z * z') (z * z' + z' * z' + z * z) Hx Lzz' (SNo_add_SNo_3 (z * z') (z' * z') (z * z) Lzz' (SNo_mul_SNo z' z' Hz'1 Hz'1) (SNo_mul_SNo z z Hz1 Hz1)) (from left to right).
We will prove x * z * z' + x * (z * z' + z' * z' + z * z) < x * z * z' + x * z * z' + (z * z') * z * z' + x * x.
rewrite the current goal using mul_SNo_distrL x (z * z') (z' * z' + z * z) Hx Lzz' (SNo_add_SNo (z' * z') (z * z) (SNo_mul_SNo z' z' Hz'1 Hz'1) (SNo_mul_SNo z z Hz1 Hz1)) (from left to right).
We will prove x * z * z' + x * z * z' + x * (z' * z' + z * z) < x * z * z' + x * z * z' + (z * z') * z * z' + x * x.
We prove the intermediate claim Lxzz': SNo (x * z * z').
An exact proof term for the current goal is SNo_mul_SNo_3 x z z' Hx Hz1 Hz'1.
Apply add_SNo_Lt2 (x * z * z') (x * z * z' + x * (z' * z' + z * z)) (x * z * z' + (z * z') * z * z' + x * x) Lxzz' (SNo_add_SNo (x * z * z') (x * (z' * z' + z * z)) Lxzz' (SNo_mul_SNo x (z' * z' + z * z) Hx (SNo_add_SNo (z' * z') (z * z) (SNo_mul_SNo z' z' Hz'1 Hz'1) (SNo_mul_SNo z z Hz1 Hz1)))) (SNo_add_SNo_3 (x * z * z') ((z * z') * z * z') (x * x) Lxzz' (SNo_mul_SNo (z * z') (z * z') Lzz' Lzz') (SNo_mul_SNo x x Hx Hx)) to the current goal.
We will prove x * z * z' + x * (z' * z' + z * z) < x * z * z' + (z * z') * z * z' + x * x.
Apply add_SNo_Lt2 (x * z * z') (x * (z' * z' + z * z)) ((z * z') * z * z' + x * x) Lxzz' (SNo_mul_SNo x (z' * z' + z * z) Hx (SNo_add_SNo (z' * z') (z * z) (SNo_mul_SNo z' z' Hz'1 Hz'1) (SNo_mul_SNo z z Hz1 Hz1))) (SNo_add_SNo ((z * z') * z * z') (x * x) (SNo_mul_SNo (z * z') (z * z') Lzz' Lzz') (SNo_mul_SNo x x Hx Hx)) to the current goal.
We will prove x * (z' * z' + z * z) < (z * z') * z * z' + x * x.
rewrite the current goal using mul_SNo_distrL x (z' * z') (z * z) Hx (SNo_mul_SNo z' z' Hz'1 Hz'1) (SNo_mul_SNo z z Hz1 Hz1) (from left to right).
We will prove x * z' * z' + x * z * z < (z * z') * z * z' + x * x.
rewrite the current goal using mul_SNo_com x (z * z) Hx (SNo_mul_SNo z z Hz1 Hz1) (from left to right).
We will prove x * z' * z' + (z * z) * x < (z * z') * z * z' + x * x.
rewrite the current goal using add_SNo_0L ((z * z') * z * z' + x * x) (SNo_add_SNo ((z * z') * z * z') (x * x) (SNo_mul_SNo (z * z') (z * z') Lzz' Lzz') (SNo_mul_SNo x x Hx Hx)) (from right to left).
We will prove x * z' * z' + (z * z) * x < 0 + (z * z') * z * z' + x * x.
Apply add_SNo_minus_Lt1 (x * z' * z' + (z * z) * x) ((z * z') * z * z' + x * x) 0 (SNo_add_SNo (x * z' * z') ((z * z) * x) (SNo_mul_SNo x (z' * z') Hx (SNo_mul_SNo z' z' Hz'1 Hz'1)) (SNo_mul_SNo (z * z) x (SNo_mul_SNo z z Hz1 Hz1) Hx)) (SNo_add_SNo ((z * z') * z * z') (x * x) (SNo_mul_SNo (z * z') (z * z') Lzz' Lzz') (SNo_mul_SNo x x Hx Hx)) SNo_0 to the current goal.
We will prove (x * z' * z' + (z * z) * x) + - ((z * z') * z * z' + x * x) < 0.
rewrite the current goal using add_SNo_assoc (x * z' * z') ((z * z) * x) (- ((z * z') * z * z' + x * x)) (SNo_mul_SNo x (z' * z') Hx (SNo_mul_SNo z' z' Hz'1 Hz'1)) (SNo_mul_SNo (z * z) x (SNo_mul_SNo z z Hz1 Hz1) Hx) (SNo_minus_SNo ((z * z') * z * z' + x * x) (SNo_add_SNo ((z * z') * z * z') (x * x) (SNo_mul_SNo (z * z') (z * z') Lzz' Lzz') (SNo_mul_SNo x x Hx Hx))) (from right to left).
rewrite the current goal using minus_add_SNo_distr ((z * z') * z * z') (x * x) (SNo_mul_SNo (z * z') (z * z') Lzz' Lzz') (SNo_mul_SNo x x Hx Hx) (from left to right).
We will prove x * z' * z' + (z * z) * x + - (z * z') * z * z' + - x * x < 0.
rewrite the current goal using add_SNo_rotate_3_1 ((z * z) * x) (- (z * z') * z * z') (- x * x) (SNo_mul_SNo (z * z) x (SNo_mul_SNo z z Hz1 Hz1) Hx) (SNo_minus_SNo ((z * z') * z * z') (SNo_mul_SNo (z * z') (z * z') Lzz' Lzz')) (SNo_minus_SNo (x * x) (SNo_mul_SNo x x Hx Hx)) (from left to right).
We will prove x * z' * z' + - x * x + (z * z) * x + - (z * z') * z * z' < 0.
rewrite the current goal using add_SNo_com ((z * z) * x) (- (z * z') * z * z') (SNo_mul_SNo (z * z) x (SNo_mul_SNo z z Hz1 Hz1) Hx) (SNo_minus_SNo ((z * z') * z * z') (SNo_mul_SNo (z * z') (z * z') Lzz' Lzz')) (from left to right).
We will prove x * z' * z' + - x * x + - (z * z') * z * z' + (z * z) * x < 0.
rewrite the current goal using mul_SNo_assoc z z' (z * z') Hz1 Hz'1 Lzz' (from right to left).
We will prove x * z' * z' + - x * x + - z * z' * z * z' + (z * z) * x < 0.
rewrite the current goal using mul_SNo_com_3_0_1 z' z z' Hz'1 Hz1 Hz'1 (from left to right).
We will prove x * z' * z' + - x * x + - z * z * z' * z' + (z * z) * x < 0.
rewrite the current goal using mul_SNo_assoc z z (z' * z') Hz1 Hz1 (SNo_mul_SNo z' z' Hz'1 Hz'1) (from left to right).
rewrite the current goal using SNo_foil_mm x (z * z) (z' * z') x Hx (SNo_mul_SNo z z Hz1 Hz1) (SNo_mul_SNo z' z' Hz'1 Hz'1) Hx (from right to left).
We will prove (x + - z * z) * (z' * z' + - x) < 0.
Apply mul_SNo_neg_pos (x + - z * z) (z' * z' + - x) (SNo_add_SNo x (- z * z) Hx (SNo_minus_SNo (z * z) (SNo_mul_SNo z z Hz1 Hz1))) (SNo_add_SNo (z' * z') (- x) (SNo_mul_SNo z' z' Hz'1 Hz'1) (SNo_minus_SNo x Hx)) to the current goal.
We will prove x + - z * z < 0.
Apply add_SNo_minus_Lt1b x (z * z) 0 Hx (SNo_mul_SNo z z Hz1 Hz1) SNo_0 to the current goal.
We will prove x < 0 + z * z.
rewrite the current goal using add_SNo_0L (z * z) (SNo_mul_SNo z z Hz1 Hz1) (from left to right).
We will prove x < z * z.
An exact proof term for the current goal is Hz3.
We will prove 0 < z' * z' + - x.
An exact proof term for the current goal is SNoLt_minus_pos x (z' * z') Hx (SNo_mul_SNo z' z' Hz'1 Hz'1) Hz'3.
An exact proof term for the current goal is Hx.
We will prove SNo (z * z').
An exact proof term for the current goal is Lzz'.
∎