Beginning of Section SurrealSqrt
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use :/: as an infix operator with priority 353 and no associativity corresponding to applying term div_SNo.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use ≤ as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
Definition. We define SNoL_nonneg to be λx ⇒ {w ∈ SNoL x|0 ≤ w} of type set → set.
In Proofgold the corresponding term root is 426e35... and object id is 1ec1d7...
Theorem. (SNoL_nonneg_0)
SNoL_nonneg 0 = 0
In Proofgold the corresponding term root is ab6dce... and proposition id is 67aa58...
Proof:
We will prove {w ∈ SNoL 0|0 ≤ w} = 0.
rewrite the current goal using SNoL_0 (from left to right).
An exact proof term for the current goal is Sep_Empty (λw ⇒ 0 ≤ w).
∎
Theorem. (SNoL_nonneg_1)
SNoL_nonneg 1 = 1
In Proofgold the corresponding term root is 74d4e8... and proposition id is e3fc28...
Proof:
We will prove {w ∈ SNoL 1|0 ≤ w} = 1.
rewrite the current goal using SNoL_1 (from left to right).
We will prove {w ∈ 1|0 ≤ w} = 1.
Apply set_ext to the current goal.
An exact proof term for the current goal is Sep_Subq 1 (λw ⇒ 0 ≤ w).
Let w be given.
Assume Hw: w ∈ 1.
Apply cases_1 w Hw to the current goal.
We will prove 0 ∈ {w ∈ 1|0 ≤ w}.
Apply SepI to the current goal.
An exact proof term for the current goal is In_0_1.
We will prove 0 ≤ 0.
Apply SNoLe_ref to the current goal.
∎
Definition. We define SNo_sqrtauxset to be λY Z x ⇒ ⋃y ∈ Y{(x + y * z) :/: (y + z)|z ∈ Z, 0 < y + z} of type set → set → set → set.
In Proofgold the corresponding term root is 211c64... and object id is 3fc62b...
Theorem. (SNo_sqrtauxset_I)
∀Y Z x, ∀y ∈ Y, ∀z ∈ Z, 0 < y + z → (x + y * z) :/: (y + z) ∈ SNo_sqrtauxset Y Z x
In Proofgold the corresponding term root is 4b16a1... and proposition id is c09ca4...
Proof:
Let Y, Z, x and y be given.
Assume Hy.
Let z be given.
Assume Hz.
Assume H1.
We will prove (x + y * z) :/: (y + z) ∈ ⋃y ∈ Y{(x + y * z) :/: (y + z)|z ∈ Z, 0 < y + z}.
Apply famunionI Y (λy ⇒ {(x + y * z) :/: (y + z)|z ∈ Z, 0 < y + z}) y ((x + y * z) :/: (y + z)) Hy to the current goal.
We will prove (x + y * z) :/: (y + z) ∈ {(x + y * z) :/: (y + z)|z ∈ Z, 0 < y + z}.
An exact proof term for the current goal is ReplSepI Z (λz ⇒ 0 < y + z) (λz ⇒ (x + y * z) :/: (y + z)) z Hz H1.
∎
Theorem. (SNo_sqrtauxset_E)
∀Y Z x, ∀u ∈ SNo_sqrtauxset Y Z x, ∀p : prop, (∀y ∈ Y, ∀z ∈ Z, 0 < y + z → u = (x + y * z) :/: (y + z) → p) → p
In Proofgold the corresponding term root is 0bec9e... and proposition id is b7810c...
Proof:
Let Y, Z, x and u be given.
Assume Hu.
Let p be given.
Assume H1.
Apply famunionE_impred Y (λy ⇒ {(x + y * z) :/: (y + z)|z ∈ Z, 0 < y + z}) u Hu to the current goal.
Let y be given.
Assume Hy: y ∈ Y.
Assume Hu1.
Apply ReplSepE_impred Z (λz ⇒ 0 < y + z) (λz ⇒ (x + y * z) :/: (y + z)) u Hu1 to the current goal.
Let z be given.
Assume Hz: z ∈ Z.
Assume Hyz: 0 < y + z.
Assume Hu2: u = (x + y * z) :/: (y + z).
An exact proof term for the current goal is H1 y Hy z Hz Hyz Hu2.
∎
Theorem. (SNo_sqrtauxset_0)
∀Z x, SNo_sqrtauxset 0 Z x = 0
In Proofgold the corresponding term root is 2d39ce... and proposition id is db93fb...
Proof:
Let Z and x be given.
Apply Empty_eq to the current goal.
Let u be given.
Assume Hu.
Apply SNo_sqrtauxset_E 0 Z x u Hu to the current goal.
Let y be given.
Assume Hy: y ∈ 0.
We will prove False.
An exact proof term for the current goal is EmptyE y Hy.
∎
Theorem. (SNo_sqrtauxset_0')
∀Y x, SNo_sqrtauxset Y 0 x = 0
In Proofgold the corresponding term root is b0f585... and proposition id is d57918...
Proof:
Let Y and x be given.
Apply Empty_eq to the current goal.
Let u be given.
Assume Hu.
Apply SNo_sqrtauxset_E Y 0 x u Hu to the current goal.
Let y be given.
Assume Hy: y ∈ Y.
Let z be given.
Assume Hz: z ∈ 0.
We will prove False.
An exact proof term for the current goal is EmptyE z Hz.
∎
Definition. We define SNo_sqrtaux to be λx g ⇒ nat_primrec ({g w|w ∈ SNoL_nonneg x},{g z|z ∈ SNoR x}) (λk p ⇒ (p 0 ∪ SNo_sqrtauxset (p 0) (p 1) x,p 1 ∪ SNo_sqrtauxset (p 0) (p 0) x ∪ SNo_sqrtauxset (p 1) (p 1) x)) of type set → (set → set) → set → set.
In Proofgold the corresponding term root is e233df... and object id is 2ebc89...
Theorem. (SNo_sqrtaux_0)
∀x, ∀g : set → set, SNo_sqrtaux x g 0 = ({g w|w ∈ SNoL_nonneg x},{g z|z ∈ SNoR x})
In Proofgold the corresponding term root is d46ed0... and proposition id is 182e5e...
Proof:
Let x and g be given.
An exact proof term for the current goal is nat_primrec_0 ({g w|w ∈ SNoL_nonneg x},{g z|z ∈ SNoR x}) (λk p ⇒ (p 0 ∪ SNo_sqrtauxset (p 0) (p 1) x,p 1 ∪ SNo_sqrtauxset (p 0) (p 0) x ∪ SNo_sqrtauxset (p 1) (p 1) x)).
∎
Theorem. (SNo_sqrtaux_S)
∀x, ∀g : set → set, ∀n, nat_p n → SNo_sqrtaux x g (ordsucc n) = (SNo_sqrtaux x g n 0 ∪ SNo_sqrtauxset (SNo_sqrtaux x g n 0) (SNo_sqrtaux x g n 1) x,SNo_sqrtaux x g n 1 ∪ SNo_sqrtauxset (SNo_sqrtaux x g n 0) (SNo_sqrtaux x g n 0) x ∪ SNo_sqrtauxset (SNo_sqrtaux x g n 1) (SNo_sqrtaux x g n 1) x)
In Proofgold the corresponding term root is bb0dd8... and proposition id is 7223d6...
Proof:
Let x, g and n be given.
Assume Hn.
An exact proof term for the current goal is nat_primrec_S ({g w|w ∈ SNoL_nonneg x},{g z|z ∈ SNoR x}) (λk p ⇒ (p 0 ∪ SNo_sqrtauxset (p 0) (p 1) x,p 1 ∪ SNo_sqrtauxset (p 0) (p 0) x ∪ SNo_sqrtauxset (p 1) (p 1) x)) n Hn.
∎
Theorem. (SNo_sqrtaux_mon_lem)
∀x, ∀g : set → set, ∀m, nat_p m → ∀n, nat_p n → SNo_sqrtaux x g m 0 ⊆ SNo_sqrtaux x g (add_nat m n) 0 ∧ SNo_sqrtaux x g m 1 ⊆ SNo_sqrtaux x g (add_nat m n) 1
In Proofgold the corresponding term root is be3c0c... and proposition id is 75cbc1...
Proof:
Let x, g and m be given.
Assume Hm.
Apply nat_ind to the current goal.
We will prove SNo_sqrtaux x g m 0 ⊆ SNo_sqrtaux x g (add_nat m 0) 0 ∧ SNo_sqrtaux x g m 1 ⊆ SNo_sqrtaux x g (add_nat m 0) 1.
rewrite the current goal using add_nat_0R m (from left to right).
We will prove SNo_sqrtaux x g m 0 ⊆ SNo_sqrtaux x g m 0 ∧ SNo_sqrtaux x g m 1 ⊆ SNo_sqrtaux x g m 1.
Apply andI to the current goal.
Apply Subq_ref to the current goal.
Apply Subq_ref to the current goal.
Let n be given.
Assume Hn IH.
Apply IH to the current goal.
Assume IH0: SNo_sqrtaux x g m 0 ⊆ SNo_sqrtaux x g (add_nat m n) 0.
Assume IH1: SNo_sqrtaux x g m 1 ⊆ SNo_sqrtaux x g (add_nat m n) 1.
rewrite the current goal using add_nat_SR m n Hn (from left to right).
We will prove SNo_sqrtaux x g m 0 ⊆ SNo_sqrtaux x g (ordsucc (add_nat m n)) 0 ∧ SNo_sqrtaux x g m 1 ⊆ SNo_sqrtaux x g (ordsucc (add_nat m n)) 1.
rewrite the current goal using SNo_sqrtaux_S x g (add_nat m n) (add_nat_p m Hm n Hn) (from left to right).
rewrite the current goal using tuple_2_0_eq (from left to right).
rewrite the current goal using tuple_2_1_eq (from left to right).
Apply andI to the current goal.
We will prove SNo_sqrtaux x g m 0 ⊆ SNo_sqrtaux x g (add_nat m n) 0 ∪ SNo_sqrtauxset (SNo_sqrtaux x g (add_nat m n) 0) (SNo_sqrtaux x g (add_nat m n) 1) x.
Apply Subq_tra (SNo_sqrtaux x g m 0) (SNo_sqrtaux x g (add_nat m n) 0) (SNo_sqrtaux x g (add_nat m n) 0 ∪ SNo_sqrtauxset (SNo_sqrtaux x g (add_nat m n) 0) (SNo_sqrtaux x g (add_nat m n) 1) x) IH0 to the current goal.
Apply binunion_Subq_1 to the current goal.
We will prove SNo_sqrtaux x g m 1 ⊆ SNo_sqrtaux x g (add_nat m n) 1 ∪ SNo_sqrtauxset (SNo_sqrtaux x g (add_nat m n) 0) (SNo_sqrtaux x g (add_nat m n) 0) x ∪ SNo_sqrtauxset (SNo_sqrtaux x g (add_nat m n) 1) (SNo_sqrtaux x g (add_nat m n) 1) x.
Apply Subq_tra (SNo_sqrtaux x g m 1) (SNo_sqrtaux x g (add_nat m n) 1) (SNo_sqrtaux x g (add_nat m n) 1 ∪ SNo_sqrtauxset (SNo_sqrtaux x g (add_nat m n) 0) (SNo_sqrtaux x g (add_nat m n) 0) x ∪ SNo_sqrtauxset (SNo_sqrtaux x g (add_nat m n) 1) (SNo_sqrtaux x g (add_nat m n) 1) x) IH1 to the current goal.
Apply Subq_tra (SNo_sqrtaux x g (add_nat m n) 1) (SNo_sqrtaux x g (add_nat m n) 1 ∪ SNo_sqrtauxset (SNo_sqrtaux x g (add_nat m n) 0) (SNo_sqrtaux x g (add_nat m n) 0) x) (SNo_sqrtaux x g (add_nat m n) 1 ∪ SNo_sqrtauxset (SNo_sqrtaux x g (add_nat m n) 0) (SNo_sqrtaux x g (add_nat m n) 0) x ∪ SNo_sqrtauxset (SNo_sqrtaux x g (add_nat m n) 1) (SNo_sqrtaux x g (add_nat m n) 1) x) to the current goal.
Apply binunion_Subq_1 to the current goal.
Apply binunion_Subq_1 to the current goal.
∎
Theorem. (SNo_sqrtaux_mon)
∀x, ∀g : set → set, ∀m, nat_p m → ∀n, nat_p n → m ⊆ n → SNo_sqrtaux x g m 0 ⊆ SNo_sqrtaux x g n 0 ∧ SNo_sqrtaux x g m 1 ⊆ SNo_sqrtaux x g n 1
In Proofgold the corresponding term root is 53a992... and proposition id is f80eb0...
Proof:
Let x, g and m be given.
Assume Hm.
Let n be given.
Assume Hn Hmn.
Apply nat_Subq_add_ex m Hm n Hn Hmn to the current goal.
Let k be given.
Assume H.
Apply H to the current goal.
Assume Hk: nat_p k.
rewrite the current goal using add_nat_com k Hk m Hm (from left to right).
Assume H1: n = add_nat m k.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is SNo_sqrtaux_mon_lem x g m Hm k Hk.
∎
Theorem. (SNo_sqrtaux_ext)
∀x, SNo x → ∀g h : set → set, (∀x' ∈ SNoS_ (SNoLev x), g x' = h x') → ∀k, nat_p k → SNo_sqrtaux x g k = SNo_sqrtaux x h k
In Proofgold the corresponding term root is 9e623f... and proposition id is 88e0ac...
Proof:
Let x be given.
Assume Hx.
Let g and h be given.
Assume Hgh.
Apply nat_ind to the current goal.
We will prove SNo_sqrtaux x g 0 = SNo_sqrtaux x h 0.
rewrite the current goal using SNo_sqrtaux_0 x g (from left to right).
rewrite the current goal using SNo_sqrtaux_0 x h (from left to right).
We will prove ({g w|w ∈ SNoL_nonneg x},{g z|z ∈ SNoR x}) = ({h w|w ∈ SNoL_nonneg x},{h z|z ∈ SNoR x}).
We prove the intermediate claim L1: {g w|w ∈ SNoL_nonneg x} = {h w|w ∈ SNoL_nonneg x}.
Apply ReplEq_ext (SNoL_nonneg x) g h to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL_nonneg x.
We will prove g w = h w.
Apply SNoL_E x Hx w (SepE1 (SNoL x) (λw ⇒ 0 ≤ w) w Hw) to the current goal.
Assume Hw1 Hw2 Hw3.
Apply Hgh to the current goal.
We will prove w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 w x Hw1 Hx Hw2.
We prove the intermediate claim L2: {g w|w ∈ SNoR x} = {h w|w ∈ SNoR x}.
Apply ReplEq_ext (SNoR x) g h to the current goal.
Let w be given.
Assume Hw: w ∈ SNoR x.
We will prove g w = h w.
Apply SNoR_E x Hx w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
Apply Hgh to the current goal.
We will prove w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 w x Hw1 Hx Hw2.
rewrite the current goal using L1 (from left to right).
rewrite the current goal using L2 (from left to right).
Use reflexivity.
Let k be given.
Assume Hk: nat_p k.
Assume IH: SNo_sqrtaux x g k = SNo_sqrtaux x h k.
We will prove SNo_sqrtaux x g (ordsucc k) = SNo_sqrtaux x h (ordsucc k).
rewrite the current goal using SNo_sqrtaux_S x g k Hk (from left to right).
rewrite the current goal using SNo_sqrtaux_S x h k Hk (from left to right).
rewrite the current goal using IH (from left to right).
Use reflexivity.
∎
Beginning of Section sqrt_SNo_nonneg
Let G : set → (set → set) → set ≝ λx g ⇒ SNoCut (⋃k ∈ ωSNo_sqrtaux x g k 0) (⋃k ∈ ωSNo_sqrtaux x g k 1)
Definition. We define sqrt_SNo_nonneg to be SNo_rec_i G of type set → set.
In Proofgold the corresponding term root is 71d152... and object id is 20211a...
Theorem. (sqrt_SNo_nonneg_eq)
∀x, SNo x → sqrt_SNo_nonneg x = G x sqrt_SNo_nonneg
In Proofgold the corresponding term root is 63c3e8... and proposition id is edc75b...
Proof:
Apply SNo_rec_i_eq G to the current goal.
Let x be given.
Assume Hx.
Let g and h be given.
Assume Hgh.
We will prove SNoCut (⋃k ∈ ωSNo_sqrtaux x g k 0) (⋃k ∈ ωSNo_sqrtaux x g k 1) = SNoCut (⋃k ∈ ωSNo_sqrtaux x h k 0) (⋃k ∈ ωSNo_sqrtaux x h k 1).
Use f_equal.
Apply famunion_ext to the current goal.
Let k be given.
Assume Hk.
We will prove SNo_sqrtaux x g k 0 = SNo_sqrtaux x h k 0.
Use f_equal.
Apply SNo_sqrtaux_ext x Hx g h to the current goal.
We will prove ∀w ∈ SNoS_ (SNoLev x), g w = h w.
An exact proof term for the current goal is Hgh.
An exact proof term for the current goal is omega_nat_p k Hk.
Apply famunion_ext to the current goal.
Let k be given.
Assume Hk.
We will prove SNo_sqrtaux x g k 1 = SNo_sqrtaux x h k 1.
Use f_equal.
Apply SNo_sqrtaux_ext x Hx g h to the current goal.
We will prove ∀w ∈ SNoS_ (SNoLev x), g w = h w.
An exact proof term for the current goal is Hgh.
An exact proof term for the current goal is omega_nat_p k Hk.
∎
Theorem. (sqrt_SNo_nonneg_prop1a)
∀x, SNo x → 0 ≤ x → (∀w ∈ SNoS_ (SNoLev x), 0 ≤ w → SNo (sqrt_SNo_nonneg w) ∧ 0 ≤ sqrt_SNo_nonneg w ∧ sqrt_SNo_nonneg w * sqrt_SNo_nonneg w = w) → ∀k, nat_p k → (∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 0, SNo y ∧ 0 ≤ y ∧ y * y < x) ∧ (∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 1, SNo y ∧ 0 ≤ y ∧ x < y * y)
In Proofgold the corresponding term root is 111bf5... and proposition id is 44bfa1...
Proof:
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'.
∎
Theorem. (sqrt_SNo_nonneg_prop1b)
∀x, SNo x → 0 ≤ x → (∀k, nat_p k → (∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 0, SNo y ∧ 0 ≤ y ∧ y * y < x) ∧ (∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 1, SNo y ∧ 0 ≤ y ∧ x < y * y)) → SNoCutP (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 0) (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 1)
In Proofgold the corresponding term root is 79d32b... and proposition id is 3a96af...
Proof:
Let x be given.
Assume Hx Hxnonneg.
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.
Assume H0: ∀k, nat_p k → (∀y ∈ L_ k, SNo y ∧ 0 ≤ y ∧ y * y < x) ∧ (∀y ∈ R_ k, SNo y ∧ 0 ≤ y ∧ x < y * y).
We will prove (∀x ∈ L, SNo x) ∧ (∀y ∈ R, SNo y) ∧ (∀x ∈ L, ∀y ∈ R, x < y).
Apply and3I to the current goal.
Let w be given.
Assume Hw: w ∈ L.
Apply famunionE_impred ω L_ w Hw to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume H1: w ∈ L_ k.
Apply H0 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.
Assume H3 _.
An exact proof term for the current goal is H3.
Let z be given.
Assume Hz: z ∈ R.
Apply famunionE_impred ω R_ z Hz to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume H1: z ∈ R_ k.
Apply H0 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.
Assume H3 _.
An exact proof term for the current goal is H3.
Let w be given.
Assume Hw: w ∈ L.
Let z be given.
Assume Hz: z ∈ R.
We will prove w < z.
Apply famunionE_impred ω L_ w Hw to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume H1: w ∈ L_ k.
Apply H0 k (omega_nat_p k Hk) to the current goal.
Assume H2 _.
Apply H2 w H1 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 famunionE_impred ω R_ z Hz to the current goal.
Let k' be given.
Assume Hk': k' ∈ ω.
Assume H3: z ∈ R_ k'.
Apply H0 k' (omega_nat_p k' Hk') to the current goal.
Assume _ H4.
Apply H4 z H3 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 w < z.
Apply SNoLtLe_or w z Hw1 Hz1 to the current goal.
Assume H5: w < z.
An exact proof term for the current goal is H5.
Assume H5: z ≤ w.
We will prove False.
Apply SNoLt_irref x to the current goal.
We will prove x < x.
Apply SNoLt_tra x (z * z) x Hx (SNo_mul_SNo z z Hz1 Hz1) Hx Hz3 to the current goal.
We will prove z * z < x.
Apply SNoLeLt_tra (z * z) (w * w) x (SNo_mul_SNo z z Hz1 Hz1) (SNo_mul_SNo w w Hw1 Hw1) Hx to the current goal.
We will prove z * z ≤ w * w.
An exact proof term for the current goal is nonneg_mul_SNo_Le2 z z w w Hz1 Hz1 Hw1 Hw1 Hz2 Hz2 H5 H5.
An exact proof term for the current goal is Hw3.
∎
Theorem. (sqrt_SNo_nonneg_prop1c)
∀x, SNo x → 0 ≤ x → SNoCutP (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 0) (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 1) → (∀z ∈ (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 1), ∀p : prop, (SNo z → 0 ≤ z → x < z * z → p) → p) → 0 ≤ G x sqrt_SNo_nonneg
In Proofgold the corresponding term root is afcc07... and proposition id is abe562...
Proof:
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.
∎
Theorem. (sqrt_SNo_nonneg_prop1d)
∀x, SNo x → 0 ≤ x → (∀w ∈ SNoS_ (SNoLev x), 0 ≤ w → SNo (sqrt_SNo_nonneg w) ∧ 0 ≤ sqrt_SNo_nonneg w ∧ sqrt_SNo_nonneg w * sqrt_SNo_nonneg w = w) → SNoCutP (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 0) (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 1) → 0 ≤ G x sqrt_SNo_nonneg → G x sqrt_SNo_nonneg * G x sqrt_SNo_nonneg < x → False
In Proofgold the corresponding term root is 9308b8... and proposition id is 9979dd...
Proof:
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.
∎
Theorem. (sqrt_SNo_nonneg_prop1e)
∀x, SNo x → 0 ≤ x → (∀w ∈ SNoS_ (SNoLev x), 0 ≤ w → SNo (sqrt_SNo_nonneg w) ∧ 0 ≤ sqrt_SNo_nonneg w ∧ sqrt_SNo_nonneg w * sqrt_SNo_nonneg w = w) → SNoCutP (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 0) (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 1) → 0 ≤ G x sqrt_SNo_nonneg → x < G x sqrt_SNo_nonneg * G x sqrt_SNo_nonneg → False
In Proofgold the corresponding term root is bd498d... and proposition id is c07c4e...
Proof:
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.
∎
Theorem. (sqrt_SNo_nonneg_prop1)
∀x, SNo x → 0 ≤ x → SNo (sqrt_SNo_nonneg x) ∧ 0 ≤ sqrt_SNo_nonneg x ∧ sqrt_SNo_nonneg x * sqrt_SNo_nonneg x = x
In Proofgold the corresponding term root is db6879... and proposition id is b09b96...
Proof:
Apply SNoLev_ind to the current goal.
Let x be given.
Assume Hx: SNo x.
Assume IH: ∀w ∈ SNoS_ (SNoLev x), 0 ≤ w → SNo (sqrt_SNo_nonneg w) ∧ 0 ≤ sqrt_SNo_nonneg w ∧ sqrt_SNo_nonneg w * sqrt_SNo_nonneg w = w.
Assume Hxnonneg: 0 ≤ x.
We will prove SNo (sqrt_SNo_nonneg x) ∧ 0 ≤ sqrt_SNo_nonneg x ∧ sqrt_SNo_nonneg x * sqrt_SNo_nonneg x = x.
rewrite the current goal using sqrt_SNo_nonneg_eq x Hx (from left to right).
We will prove SNo (G x sqrt_SNo_nonneg) ∧ 0 ≤ G x sqrt_SNo_nonneg ∧ G x sqrt_SNo_nonneg * G x sqrt_SNo_nonneg = x.
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 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.
We prove the intermediate claim L2: SNoCutP L R.
An exact proof term for the current goal is sqrt_SNo_nonneg_prop1b x Hx Hxnonneg L1.
Apply L2 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.
Set y to be the term SNoCut L R.
Apply SNoCutP_SNoCut_impred L R L2 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 Lynn: 0 ≤ y.
An exact proof term for the current goal is sqrt_SNo_nonneg_prop1c x Hx Hxnonneg L2 L1R.
We will prove SNo y ∧ 0 ≤ y ∧ y * y = x.
Apply and3I to the current goal.
We will prove SNo y.
An exact proof term for the current goal is H1.
We will prove 0 ≤ y.
An exact proof term for the current goal is Lynn.
We will prove y * y = x.
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 Lynn Lynn.
Apply SNoLt_trichotomy_or_impred (y * y) x Lyy Hx to the current goal.
Assume H6: y * y < x.
We will prove False.
An exact proof term for the current goal is sqrt_SNo_nonneg_prop1d x Hx Hxnonneg IH L2 Lynn H6.
Assume H6: y * y = x.
An exact proof term for the current goal is H6.
Assume H6: x < y * y.
We will prove False.
An exact proof term for the current goal is sqrt_SNo_nonneg_prop1e x Hx Hxnonneg IH L2 Lynn H6.
∎
End of Section sqrt_SNo_nonneg
Theorem. (SNo_sqrtaux_0_1_prop)
∀x, SNo x → 0 ≤ x → ∀k, nat_p k → (∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 0, SNo y ∧ 0 ≤ y ∧ y * y < x) ∧ (∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 1, SNo y ∧ 0 ≤ y ∧ x < y * y)
In Proofgold the corresponding term root is 955f65... and proposition id is a2bb45...
Proof:
Let x be given.
Assume Hx Hxnonneg.
Apply sqrt_SNo_nonneg_prop1a x Hx Hxnonneg to the current goal.
Let w be given.
Assume Hw Hwnonneg.
Apply SNoS_E2 (SNoLev x) (SNoLev_ordinal x Hx) w Hw to the current goal.
Assume Hw1 Hw2 Hw3 Hw4.
An exact proof term for the current goal is sqrt_SNo_nonneg_prop1 w Hw3 Hwnonneg.
∎
Theorem. (SNo_sqrtaux_0_prop)
∀x, SNo x → 0 ≤ x → ∀k, nat_p k → ∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 0, SNo y ∧ 0 ≤ y ∧ y * y < x
In Proofgold the corresponding term root is abda0d... and proposition id is 8db9d4...
Proof:
Let x be given.
Assume Hx Hxnonneg.
Let k be given.
Assume Hk.
Apply SNo_sqrtaux_0_1_prop x Hx Hxnonneg k Hk to the current goal.
Assume H _.
An exact proof term for the current goal is H.
∎
Theorem. (SNo_sqrtaux_1_prop)
∀x, SNo x → 0 ≤ x → ∀k, nat_p k → ∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 1, SNo y ∧ 0 ≤ y ∧ x < y * y
In Proofgold the corresponding term root is d59bfa... and proposition id is 95a41e...
Proof:
Let x be given.
Assume Hx Hxnonneg.
Let k be given.
Assume Hk.
Apply SNo_sqrtaux_0_1_prop x Hx Hxnonneg k Hk to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
∎
Theorem. (SNo_sqrt_SNo_SNoCutP)
∀x, SNo x → 0 ≤ x → SNoCutP (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 0) (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 1)
In Proofgold the corresponding term root is 33c123... and proposition id is d04ad9...
Proof:
Let x be given.
Assume Hx Hxnonneg.
Apply sqrt_SNo_nonneg_prop1b x Hx Hxnonneg to the current goal.
An exact proof term for the current goal is SNo_sqrtaux_0_1_prop x Hx Hxnonneg.
∎
Theorem. (SNo_sqrt_SNo_nonneg)
∀x, SNo x → 0 ≤ x → SNo (sqrt_SNo_nonneg x)
In Proofgold the corresponding term root is 016da2... and proposition id is c5c4da...
Proof:
Let x be given.
Assume Hx Hxnonneg.
Apply sqrt_SNo_nonneg_prop1 x Hx Hxnonneg to the current goal.
Assume H _.
Apply H to the current goal.
Assume H _.
An exact proof term for the current goal is H.
∎
Theorem. (sqrt_SNo_nonneg_nonneg)
∀x, SNo x → 0 ≤ x → 0 ≤ sqrt_SNo_nonneg x
In Proofgold the corresponding term root is 40638f... and proposition id is 6c1cd0...
Proof:
Let x be given.
Assume Hx Hxnonneg.
Apply sqrt_SNo_nonneg_prop1 x Hx Hxnonneg to the current goal.
Assume H _.
Apply H to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
∎
Theorem. (sqrt_SNo_nonneg_sqr)
∀x, SNo x → 0 ≤ x → sqrt_SNo_nonneg x * sqrt_SNo_nonneg x = x
In Proofgold the corresponding term root is c79d06... and proposition id is 15814c...
Proof:
Let x be given.
Assume Hx Hxnonneg.
Apply sqrt_SNo_nonneg_prop1 x Hx Hxnonneg to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
∎
Theorem. (sqrt_SNo_nonneg_0)
sqrt_SNo_nonneg 0 = 0
In Proofgold the corresponding term root is 0afb2a... and proposition id is c6b1a7...
Proof:
rewrite the current goal using sqrt_SNo_nonneg_eq 0 SNo_0 (from left to right).
Set L_ to be the term λk : set ⇒ SNo_sqrtaux 0 sqrt_SNo_nonneg k 0.
Set R_ to be the term λk : set ⇒ SNo_sqrtaux 0 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 SNoCut L R = 0.
We prove the intermediate claim L1: ∀k, nat_p k → L_ k = 0 ∧ R_ k = 0.
Apply nat_ind to the current goal.
Apply andI to the current goal.
We will prove L_ 0 = 0.
We will prove SNo_sqrtaux 0 sqrt_SNo_nonneg 0 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 w|w ∈ SNoL_nonneg 0} = 0.
rewrite the current goal using SNoL_nonneg_0 (from left to right).
An exact proof term for the current goal is Repl_Empty sqrt_SNo_nonneg.
We will prove R_ 0 = 0.
We will prove SNo_sqrtaux 0 sqrt_SNo_nonneg 0 1 = 0.
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 w|w ∈ SNoR 0} = 0.
rewrite the current goal using SNoR_0 (from left to right).
An exact proof term for the current goal is Repl_Empty sqrt_SNo_nonneg.
Let k be given.
Assume Hk.
Assume IHk.
Apply IHk to the current goal.
Assume IHLk: L_ k = 0.
Assume IHRk: R_ k = 0.
Apply andI to the current goal.
We will prove L_ (ordsucc k) = 0.
We will prove SNo_sqrtaux 0 sqrt_SNo_nonneg (ordsucc k) 0 = 0.
rewrite the current goal using SNo_sqrtaux_S 0 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 L_ k ∪ SNo_sqrtauxset (L_ k) (R_ k) 0 = Empty.
rewrite the current goal using IHLk (from left to right).
We will prove 0 ∪ SNo_sqrtauxset 0 (R_ k) 0 = Empty.
Apply SNo_sqrtauxset_0 (R_ k) 0 (λ_ u ⇒ 0 ∪ u = 0) to the current goal.
We will prove 0 ∪ 0 = Empty.
Apply binunion_idl to the current goal.
We will prove R_ (ordsucc k) = 0.
We will prove SNo_sqrtaux 0 sqrt_SNo_nonneg (ordsucc k) 1 = 0.
rewrite the current goal using SNo_sqrtaux_S 0 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 R_ k ∪ SNo_sqrtauxset (L_ k) (L_ k) 0 ∪ SNo_sqrtauxset (R_ k) (R_ k) 0 = Empty.
rewrite the current goal using IHLk (from left to right).
rewrite the current goal using IHRk (from left to right).
We will prove 0 ∪ SNo_sqrtauxset 0 0 0 ∪ SNo_sqrtauxset 0 0 0 = Empty.
rewrite the current goal using SNo_sqrtauxset_0 0 0 (from left to right).
We will prove 0 ∪ 0 ∪ 0 = Empty.
rewrite the current goal using binunion_idl 0 (from left to right).
We will prove 0 ∪ 0 = Empty.
Apply binunion_idl to the current goal.
We prove the intermediate claim L2: L = 0.
Apply Empty_eq to the current goal.
Let x be given.
Assume Hx: x ∈ L.
Apply famunionE_impred ω L_ x Hx to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Apply L1 k (omega_nat_p k Hk) to the current goal.
Assume H1: L_ k = 0.
Assume _.
We will prove x ∉ L_ k.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is EmptyE x.
We prove the intermediate claim L3: R = 0.
Apply Empty_eq to the current goal.
Let x be given.
Assume Hx: x ∈ R.
Apply famunionE_impred ω R_ x Hx to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Apply L1 k (omega_nat_p k Hk) to the current goal.
Assume _.
Assume H1: R_ k = 0.
We will prove x ∉ R_ k.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is EmptyE x.
rewrite the current goal using L2 (from left to right).
rewrite the current goal using L3 (from left to right).
An exact proof term for the current goal is SNoCut_0_0.
∎
Theorem. (sqrt_SNo_nonneg_1)
sqrt_SNo_nonneg 1 = 1
In Proofgold the corresponding term root is 1801e5... and proposition id is d5a6d5...
Proof:
rewrite the current goal using sqrt_SNo_nonneg_eq 1 SNo_1 (from left to right).
Set L_ to be the term λk : set ⇒ SNo_sqrtaux 1 sqrt_SNo_nonneg k 0.
Set R_ to be the term λk : set ⇒ SNo_sqrtaux 1 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 SNoCut L R = 1.
We prove the intermediate claim L1: ∀k, nat_p k → L_ k = 1 ∧ R_ k = 0.
Apply nat_ind to the current goal.
Apply andI to the current goal.
We will prove L_ 0 = 1.
We will prove SNo_sqrtaux 1 sqrt_SNo_nonneg 0 0 = 1.
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 w|w ∈ SNoL_nonneg 1} = 1.
rewrite the current goal using SNoL_nonneg_1 (from left to right).
We will prove {sqrt_SNo_nonneg w|w ∈ 1} = 1.
Apply set_ext to the current goal.
Let u be given.
Assume Hu: u ∈ {sqrt_SNo_nonneg w|w ∈ 1}.
We will prove u ∈ 1.
Apply ReplE_impred 1 sqrt_SNo_nonneg u Hu to the current goal.
Let w be given.
Assume Hw: w ∈ 1.
Apply cases_1 w Hw to the current goal.
rewrite the current goal using sqrt_SNo_nonneg_0 (from left to right).
Assume Hu0: u = 0.
rewrite the current goal using Hu0 (from left to right).
An exact proof term for the current goal is In_0_1.
Let u be given.
Assume Hu: u ∈ 1.
Apply cases_1 u Hu to the current goal.
We will prove 0 ∈ {sqrt_SNo_nonneg w|w ∈ 1}.
rewrite the current goal using sqrt_SNo_nonneg_0 (from right to left) at position 1.
Apply ReplI to the current goal.
An exact proof term for the current goal is In_0_1.
We will prove R_ 0 = 0.
We will prove SNo_sqrtaux 1 sqrt_SNo_nonneg 0 1 = 0.
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 w|w ∈ SNoR 1} = 0.
rewrite the current goal using SNoR_1 (from left to right).
An exact proof term for the current goal is Repl_Empty sqrt_SNo_nonneg.
Let k be given.
Assume Hk.
Assume IHk.
Apply IHk to the current goal.
Assume IHLk: L_ k = 1.
Assume IHRk: R_ k = 0.
Apply andI to the current goal.
We will prove L_ (ordsucc k) = 1.
We will prove SNo_sqrtaux 1 sqrt_SNo_nonneg (ordsucc k) 0 = 1.
rewrite the current goal using SNo_sqrtaux_S 1 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 L_ k ∪ SNo_sqrtauxset (L_ k) (R_ k) 1 = 1.
rewrite the current goal using IHLk (from left to right).
rewrite the current goal using IHRk (from left to right).
We will prove 1 ∪ SNo_sqrtauxset 1 0 1 = 1.
rewrite the current goal using SNo_sqrtauxset_0' 1 1 (from left to right).
Apply binunion_idr to the current goal.
We will prove R_ (ordsucc k) = 0.
We will prove SNo_sqrtaux 1 sqrt_SNo_nonneg (ordsucc k) 1 = 0.
rewrite the current goal using SNo_sqrtaux_S 1 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 R_ k ∪ SNo_sqrtauxset (L_ k) (L_ k) 1 ∪ SNo_sqrtauxset (R_ k) (R_ k) 1 = 0.
rewrite the current goal using IHLk (from left to right).
rewrite the current goal using IHRk (from left to right).
We will prove 0 ∪ SNo_sqrtauxset 1 1 1 ∪ SNo_sqrtauxset 0 0 1 = 0.
rewrite the current goal using SNo_sqrtauxset_0 0 1 (from left to right).
We will prove 0 ∪ SNo_sqrtauxset 1 1 1 ∪ 0 = 0.
rewrite the current goal using binunion_idl (SNo_sqrtauxset 1 1 1) (from left to right).
rewrite the current goal using binunion_idr (SNo_sqrtauxset 1 1 1) (from left to right).
We will prove SNo_sqrtauxset 1 1 1 = 0.
Apply Empty_eq to the current goal.
Let u be given.
Assume Hu: u ∈ SNo_sqrtauxset 1 1 1.
Apply SNo_sqrtauxset_E 1 1 1 u Hu to the current goal.
Let w be given.
Assume Hw: w ∈ 1.
Let z be given.
Assume Hz: z ∈ 1.
Apply cases_1 w Hw to the current goal.
Apply cases_1 z Hz to the current goal.
rewrite the current goal using add_SNo_0R 0 SNo_0 (from left to right).
Assume H1: 0 < 0.
We will prove False.
Apply SNoLt_irref 0 to the current goal.
An exact proof term for the current goal is H1.
We prove the intermediate claim L2: L = 1.
Apply set_ext to the current goal.
We will prove L ⊆ 1.
Let x be given.
Assume Hx: x ∈ L.
Apply famunionE_impred ω L_ x Hx to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Apply L1 k (omega_nat_p k Hk) to the current goal.
Assume H1: L_ k = 1.
Assume _.
We will prove x ∈ L_ k → x ∈ 1.
rewrite the current goal using H1 (from left to right).
Assume H2: x ∈ 1.
We will prove x ∈ 1.
An exact proof term for the current goal is H2.
Let x be given.
Assume Hx: x ∈ 1.
Apply cases_1 x Hx to the current goal.
We will prove 0 ∈ L.
We prove the intermediate claim L2a: 0 ∈ L_ 0.
Apply L1 0 nat_0 to the current goal.
Assume H1: L_ 0 = 1.
Assume _.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is In_0_1.
We will prove 0 ∈ ⋃k ∈ ωL_ k.
An exact proof term for the current goal is famunionI ω L_ 0 0 (nat_p_omega 0 nat_0) L2a.
We prove the intermediate claim L3: R = 0.
Apply Empty_eq to the current goal.
Let x be given.
Assume Hx: x ∈ R.
Apply famunionE_impred ω R_ x Hx to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Apply L1 k (omega_nat_p k Hk) to the current goal.
Assume _.
Assume H1: R_ k = 0.
We will prove x ∉ R_ k.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is EmptyE x.
rewrite the current goal using L2 (from left to right).
rewrite the current goal using L3 (from left to right).
We will prove SNoCut 1 0 = 1.
rewrite the current goal using SNoL_1 (from right to left) at position 1.
rewrite the current goal using SNoR_1 (from right to left) at position 2.
We will prove SNoCut (SNoL 1) (SNoR 1) = 1.
Use symmetry.
An exact proof term for the current goal is SNo_eta 1 SNo_1.
∎
End of Section SurrealSqrt