Let Y, Z and x be given.
Assume HY HZ Hx Hxnneg.
We will prove (⋃y ∈ Y{(x + y * z) :/: (y + z)|z ∈ Z, 0 < y + z}) ⊆ {w ∈ real|0 ≤ w}.
We prove the intermediate claim LY: Y ⊆ real.
Let y be given.
Assume Hy.
An exact proof term for the current goal is SepE1 real (λw ⇒ 0 ≤ w) y (HY y Hy).
We prove the intermediate claim LZ: Z ⊆ real.
Let z be given.
Assume Hz.
An exact proof term for the current goal is SepE1 real (λw ⇒ 0 ≤ w) z (HZ z Hz).
We prove the intermediate claim LxS: SNo x.
An exact proof term for the current goal is real_SNo x Hx.
Let w be given.
Assume Hw.
Apply SepI to the current goal.
Apply SNo_sqrtauxset_real Y Z x LY LZ Hx w Hw to the current goal.
We will prove 0 ≤ w.
Apply famunionE_impred Y (λy ⇒ {(x + y * z) :/: (y + z)|z ∈ Z, 0 < y + z}) w Hw to the current goal.
Let y be given.
Assume Hy: y ∈ Y.
Assume Hw2: w ∈ {(x + y * z) :/: (y + z)|z ∈ Z, 0 < y + z}.
Apply ReplSepE_impred Z (λz ⇒ 0 < y + z) (λz ⇒ (x + y * z) :/: (y + z)) w Hw2 to the current goal.
Let z be given.
Assume Hz: z ∈ Z.
Assume Hyz: 0 < y + z.
Assume Hw3: w = (x + y * z) :/: (y + z).
Apply SepE real (λw ⇒ 0 ≤ w) y (HY y Hy) to the current goal.
Assume HyR: y ∈ real.
Assume Hynneg: 0 ≤ y.
We prove the intermediate claim LyS: SNo y.
An exact proof term for the current goal is real_SNo y HyR.
Apply SepE real (λz ⇒ 0 ≤ z) z (HZ z Hz) to the current goal.
Assume HzR: z ∈ real.
Assume Hznneg: 0 ≤ z.
We prove the intermediate claim LzS: SNo z.
An exact proof term for the current goal is real_SNo z HzR.
rewrite the current goal using Hw3 (from left to right).
We will prove 0 ≤ (x + y * z) :/: (y + z).
We prove the intermediate claim L1: 0 ≤ x + y * z.
rewrite the current goal using add_SNo_0R 0 SNo_0 (from right to left).
Apply add_SNo_Le3 0 0 x (y * z) SNo_0 SNo_0 (real_SNo x Hx) (SNo_mul_SNo y z LyS LzS) to the current goal.
We will prove 0 ≤ x.
An exact proof term for the current goal is Hxnneg.
We will prove 0 ≤ y * z.
Apply SNoLeE 0 y SNo_0 LyS Hynneg to the current goal.
Assume H1: 0 < y.
Apply SNoLeE 0 z SNo_0 LzS Hznneg to the current goal.
Assume H2: 0 < z.
Apply SNoLtLe to the current goal.
We will prove 0 < y * z.
An exact proof term for the current goal is mul_SNo_pos_pos y z LyS LzS H1 H2.
Assume H2: 0 = z.
rewrite the current goal using H2 (from right to left).
rewrite the current goal using mul_SNo_zeroR y LyS (from left to right).
Apply SNoLe_ref to the current goal.
Assume H1: 0 = y.
rewrite the current goal using H1 (from right to left).
rewrite the current goal using mul_SNo_zeroL z LzS (from left to right).
Apply SNoLe_ref to the current goal.
Apply SNoLeE 0 (x + y * z) SNo_0 (SNo_add_SNo x (y * z) LxS (SNo_mul_SNo y z LyS LzS)) L1 to the current goal.
Assume H1: 0 < x + y * z.
We will prove 0 ≤ (x + y * z) :/: (y + z).
Apply SNoLtLe to the current goal.
We will prove 0 < (x + y * z) :/: (y + z).
An exact proof term for the current goal is div_SNo_pos_pos (x + y * z) (y + z) (SNo_add_SNo x (y * z) LxS (SNo_mul_SNo y z LyS LzS)) (SNo_add_SNo y z LyS LzS) H1 Hyz.
Assume H1: 0 = x + y * z.
rewrite the current goal using H1 (from right to left).
rewrite the current goal using div_SNo_0_num (y + z) (SNo_add_SNo y z LyS LzS) (from left to right).
Apply SNoLe_ref to the current goal.
∎