Modularization of BinNat + fixes of stdlib

 A sub-module N in BinNat now contains functions add (ex-Nplus),
 mul (ex-Nmult), ... and properties.

 In particular, this sub-module N directly instantiates NAxiomsSig
  and includes all derived properties NProp.

 Files Ndiv_def and co are now obsolete and kept only for compat

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

1 files changed, 8 insertions, 40 deletions

diff --git a/theories/NArith/Nsqrt_def.v b/theories/NArith/Nsqrt_def.v
index 375ed0f90..edb6b2895 100644
--- a/theories/NArith/Nsqrt_def.v
+++ b/theories/NArith/Nsqrt_def.v
@@ -6,45 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Definition of a square root function for N. *)
+Require Import BinNat.
 
-Require Import BinPos BinNat.
+(** Obsolete file, see [BinNat] now,
+    only compatibility notations remain here. *)
 
-Local Open Scope N_scope.
-
-Definition Nsqrtrem n :=
- match n with
-  | N0 => (N0, N0)
-  | Npos p =>
-    match Pos.sqrtrem p with
-     | (s, IsPos r) => (Npos s, Npos r)
-     | (s, _) => (Npos s, N0)
-    end
- end.
-
-Definition Nsqrt n :=
- match n with
-  | N0 => N0
-  | Npos p => Npos (Pos.sqrt p)
- end.
-
-Lemma Nsqrtrem_spec : forall n,
- let (s,r) := Nsqrtrem n in n = s*s + r /\ r <= 2*s.
-Proof.
- destruct n. now split.
- generalize (Pos.sqrtrem_spec p). simpl.
- destruct 1; simpl; subst; now split.
-Qed.
-
-Lemma Nsqrt_spec : forall n,
- let s := Nsqrt n in s*s <= n < (Nsucc s)*(Nsucc s).
-Proof.
- destruct n. now split. apply (Pos.sqrt_spec p).
-Qed.
-
-Lemma Nsqrtrem_sqrt : forall n, fst (Nsqrtrem n) = Nsqrt n.
-Proof.
- destruct n. reflexivity.
- unfold Nsqrtrem, Nsqrt, Pos.sqrt.
- destruct (Pos.sqrtrem p) as (s,r). now destruct r.
-Qed.
\ No newline at end of file
+Notation Nsqrtrem := N.sqrtrem (only parsing).
+Notation Nsqrt := N.sqrt (only parsing).
+Notation Nsqrtrem_spec := N.sqrtrem_spec (only parsing).
+Notation Nsqrt_spec := (fun n => N.sqrt_spec n (N.le_0_l n)) (only parsing).
+Notation Nsqrtrem_sqrt := N.sqrtrem_sqrt (only parsing).