Let x and y be given.
Assume Hx Hy Hxnn Hxy.
We prove the intermediate claim LsxS: SNo (sqrt_SNo_nonneg x).
An exact proof term for the current goal is SNo_sqrt_SNo_nonneg x ?? ??.
We prove the intermediate claim Lsxnn: 0 ≤ sqrt_SNo_nonneg x.
An exact proof term for the current goal is sqrt_SNo_nonneg_nonneg x ?? ??.
We prove the intermediate claim Lynn: 0 ≤ y.
Apply SNoLe_tra 0 x y SNo_0 ?? ?? ?? to the current goal.
We will prove x ≤ y.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hxy.
We prove the intermediate claim LsyS: SNo (sqrt_SNo_nonneg y).
An exact proof term for the current goal is SNo_sqrt_SNo_nonneg y ?? ??.
We prove the intermediate claim Lsynn: 0 ≤ sqrt_SNo_nonneg y.
An exact proof term for the current goal is sqrt_SNo_nonneg_nonneg y ?? ??.
Apply SNoLtLe_or (sqrt_SNo_nonneg x) (sqrt_SNo_nonneg y) ?? ?? to the current goal.
Assume H2.
An exact proof term for the current goal is H2.
Assume H2: sqrt_SNo_nonneg y ≤ sqrt_SNo_nonneg x.
We will prove False.
Apply SNoLt_irref x to the current goal.
We will prove x < x.
Apply SNoLtLe_tra x y x Hx Hy Hx Hxy to the current goal.
We will prove y ≤ x.
rewrite the current goal using sqrt_SNo_nonneg_sqr y ?? ?? (from right to left).
rewrite the current goal using sqrt_SNo_nonneg_sqr x ?? ?? (from right to left).
We will
prove sqrt_SNo_nonneg y * sqrt_SNo_nonneg y ≤ sqrt_SNo_nonneg x * sqrt_SNo_nonneg x.
Apply nonneg_mul_SNo_Le2 (sqrt_SNo_nonneg y) (sqrt_SNo_nonneg y) (sqrt_SNo_nonneg x) (sqrt_SNo_nonneg x) ?? ?? ?? ?? ?? ?? ?? ?? to the current goal.