Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Assume H0:
SNo
x0
.
Assume H1:
SNoLe
0
x0
.
Apply sqrt_SNo_nonneg_prop1 with
x0
,
SNoLe
0
(
sqrt_SNo_nonneg
x0
)
leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Assume H2:
and
(
SNo
(
sqrt_SNo_nonneg
x0
)
)
(
SNoLe
0
(
sqrt_SNo_nonneg
x0
)
)
.
Assume H3:
mul_SNo
(
sqrt_SNo_nonneg
x0
)
(
sqrt_SNo_nonneg
x0
)
=
x0
.
Apply H2 with
SNoLe
0
(
sqrt_SNo_nonneg
x0
)
.
Assume H4:
SNo
(
sqrt_SNo_nonneg
x0
)
.
Assume H5:
SNoLe
0
(
sqrt_SNo_nonneg
x0
)
.
The subproof is completed by applying H5.
■