Add sqrt in Numbers

 As for power recently, we add a specification in NZ,N,Z,
 derived properties, implementations for nat, N, Z, BigN, BigZ.

  - For nat, this sqrt is brand new :-), cf NPeano.v

  - For Z, we rework what was in Zsqrt: same algorithm,
    no more refine but a pure function, based now on a sqrt
    for positive, from which we derive a Nsqrt and a Zsqrt.
    For the moment, the old Zsqrt.v file is kept as Zsqrt_compat.v.
    It is not loaded by default by Require ZArith.
    New definitions are now in Psqrt.v, Zsqrt_def.v and Nsqrt_def.v

  - For BigN, BigZ, we changed the specifications to refer to Zsqrt
    instead of using characteristic inequations.

 On the way, many extensions, in particular BinPos (lemmas about order),
 NZMulOrder (results about squares)

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

1 files changed, 7 insertions, 2 deletions

diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index e2e398025..ef9057c06 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -239,9 +239,14 @@ Proof.
 apply lt_le_incl, lt_0_1.
 Qed.
 
+Theorem lt_1_2 : 1 < 2.
+Proof.
+rewrite two_succ. apply lt_succ_diag_r.
+Qed.
+
 Theorem lt_0_2 : 0 < 2.
 Proof.
-transitivity 1. apply lt_0_1. rewrite two_succ. apply lt_succ_diag_r.
+transitivity 1. apply lt_0_1. apply lt_1_2.
 Qed.
 
 Theorem le_0_2 : 0 <= 2.
@@ -256,7 +261,7 @@ Qed.
 
 (** The order tactic enriched with some knowledge of 0,1,2 *)
 
-Ltac order' := generalize lt_0_1 lt_0_2; order.
+Ltac order' := generalize lt_0_1 lt_1_2; order.
 
 
 (** More Trichotomy, decidability and double negation elimination. *)