Library Coq.ZArith.Zsqrt
Definition and properties of square root on Z
The following tactic replaces all instances of (POS (xI ...)) by
`2*(POS ...)+1`, but only when ... is not made only with xO, XI, or xH.
Define with integer input, but with a strong (readable) specification.
Define a function of type Z->Z that computes the integer square root,
but only for positive numbers, and 0 for others.
A basic theorem about Zsqrt_plain
Positivity
Direct correctness on squares.
Zsqrt_plain is increasing