Let x and y be given.
Assume Hx Hy Hxnn Hynn.
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 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 ?? ??.
We prove the intermediate
claim LsxsyS:
SNo (sqrt_SNo_nonneg x * sqrt_SNo_nonneg y).
Apply SNo_mul_SNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L1:
(sqrt_SNo_nonneg x * sqrt_SNo_nonneg y) ^ 2 = x * y.
rewrite the current goal using
exp_SNo_nat_2 (sqrt_SNo_nonneg x * sqrt_SNo_nonneg y) ?? (from left to right).
We will
prove (sqrt_SNo_nonneg x * sqrt_SNo_nonneg y) * (sqrt_SNo_nonneg x * sqrt_SNo_nonneg y) = x * y.
rewrite the current goal using mul_SNo_com_4_inner_mid (sqrt_SNo_nonneg x) (sqrt_SNo_nonneg y) (sqrt_SNo_nonneg x) (sqrt_SNo_nonneg y) ?? ?? ?? ?? (from left to right).
Use f_equal.
An exact proof term for the current goal is sqrt_SNo_nonneg_sqr x ?? ??.
An exact proof term for the current goal is sqrt_SNo_nonneg_sqr y ?? ??.
rewrite the current goal using L1 (from right to left).
We will
prove SNo (sqrt_SNo_nonneg x * sqrt_SNo_nonneg y).
An exact proof term for the current goal is LsxsyS.
We will
prove 0 ≤ sqrt_SNo_nonneg x * sqrt_SNo_nonneg y.
Apply mul_SNo_nonneg_nonneg to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.