Let x be given.
Assume Hx Hxnonneg.
Set L to be the term
⋃k ∈ ωL_ k.
Set R to be the term
⋃k ∈ ωR_ k.
Apply and3I to the current goal.
Let w be given.
Let k be given.
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.
Let k be given.
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.
Let z be given.
Let k be given.
Assume H2 _.
Apply H2 w H1 to the current goal.
Assume H.
Apply H to the current goal.
Let k' be given.
Assume _ H4.
Apply H4 z H3 to the current goal.
Assume H.
Apply H to the current goal.
An exact proof term for the current goal is H5.
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.
∎