Added alternate versions of existing lemmas on sqrt.

Indeed, since sqrt is a total function, most lemmas are true, even for
negative inputs. For instance, sqrt_le_1 was

  0 <= x -> 0 <= y -> x <= y -> sqrt x <= sqrt y

while sqrt_le_1_alt is just

  x <= y -> sqrt x <= sqrt y.

Naming is done by adding _alt suffixes. In an ideal world (Coq 9.0?), these
new lemmas should just replace the original ones.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12457 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions