1 files changed, 0 insertions, 205 deletions
diff --git a/theories7/NArith/BinNat.v b/theories7/NArith/BinNat.v
deleted file mode 100644
index 5e04e22e..00000000
--- a/theories7/NArith/BinNat.v
+++ /dev/null
@@ -1,205 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: BinNat.v,v 1.1.2.1 2004/07/16 19:31:30 herbelin Exp $ i*)
-
-Require BinPos.
-
-(**********************************************************************)
-(** Binary natural numbers *)
-
-Inductive entier: Set := Nul : entier | Pos : positive -> entier.
-
-(** Declare binding key for scope positive_scope *)
-
-Delimits Scope N_scope with N.
-
-(** Automatically open scope N_scope for the constructors of N *)
-
-Bind Scope N_scope with entier.
-Arguments Scope Pos [ N_scope ].
-
-Open Local Scope N_scope.
-
-(** Operation x -> 2*x+1 *)
-
-Definition Un_suivi_de := [x]
-  Cases x of Nul => (Pos xH) | (Pos p) => (Pos (xI p)) end.
-
-(** Operation x -> 2*x *)
-
-Definition Zero_suivi_de :=
-  [n] Cases n of Nul => Nul | (Pos p) => (Pos (xO p)) end.
-
-(** Successor *)
-
-Definition Nsucc :=
-  [n] Cases n of Nul => (Pos xH) | (Pos p) => (Pos (add_un p)) end.
-
-(** Addition *)
-
-Definition Nplus := [n,m]
-  Cases n m of
-  | Nul     _       => m
-  | _       Nul     => n
-  | (Pos p) (Pos q) => (Pos (add p q))
-  end.
-
-V8Infix "+" Nplus : N_scope.
-
-(** Multiplication *)
-
-Definition Nmult := [n,m]
-  Cases n m of
-  | Nul     _       => Nul
-  | _       Nul     => Nul
-  | (Pos p) (Pos q) => (Pos (times p q))
-  end.
-
-V8Infix "*" Nmult : N_scope.
-
-(** Order *)
-
-Definition Ncompare := [n,m]
-  Cases n m of
-  | Nul      Nul      => EGAL
-  | Nul      (Pos m') => INFERIEUR
-  | (Pos n') Nul      => SUPERIEUR
-  | (Pos n') (Pos m') => (compare n' m' EGAL)
-  end.
-
-V8Infix "?=" Ncompare (at level 70, no associativity) : N_scope.
-
-(** Peano induction on binary natural numbers *)
-
-Theorem Nind : (P:(entier ->Prop))
-  (P Nul) ->((n:entier)(P n) ->(P (Nsucc n))) ->(n:entier)(P n).
-Proof.
-NewDestruct n.
-  Assumption.
-  Apply Pind with P := [p](P (Pos p)).
-Exact (H0 Nul H).
-Intro p'; Exact (H0 (Pos p')).
-Qed.
-
-(** Properties of addition *)
-
-Theorem Nplus_0_l : (n:entier)(Nplus Nul n)=n.
-Proof.
-Reflexivity.
-Qed.
-
-Theorem Nplus_0_r : (n:entier)(Nplus n Nul)=n.
-Proof.
-NewDestruct n; Reflexivity.
-Qed.
-
-Theorem Nplus_comm : (n,m:entier)(Nplus n m)=(Nplus m n).
-Proof.
-Intros.
-NewDestruct n; NewDestruct m; Simpl; Try Reflexivity.
-Rewrite add_sym; Reflexivity.
-Qed.
-
-Theorem Nplus_assoc : 
-  (n,m,p:entier)(Nplus n (Nplus m p))=(Nplus (Nplus n m) p).
-Proof.
-Intros.
-NewDestruct n; Try Reflexivity.
-NewDestruct m; Try Reflexivity.
-NewDestruct p; Try Reflexivity.
-Simpl; Rewrite add_assoc; Reflexivity.
-Qed.
-
-Theorem Nplus_succ : (n,m:entier)(Nplus (Nsucc n) m)=(Nsucc (Nplus n m)).
-Proof.
-NewDestruct n; NewDestruct m.
-  Simpl; Reflexivity.
-  Unfold Nsucc Nplus; Rewrite <- ZL12bis; Reflexivity.
-  Simpl; Reflexivity.
-  Simpl; Rewrite ZL14bis; Reflexivity.
-Qed.
-
-Theorem Nsucc_inj : (n,m:entier)(Nsucc n)=(Nsucc m)->n=m.
-Proof.
-NewDestruct n; NewDestruct m; Simpl; Intro H; 
-  Reflexivity Orelse Injection H; Clear H; Intro H.
-  Symmetry in H; Contradiction add_un_not_un with p.
-  Contradiction add_un_not_un with p.
-  Rewrite add_un_inj with 1:=H; Reflexivity.
-Qed.
-
-Theorem Nplus_reg_l : (n,m,p:entier)(Nplus n m)=(Nplus n p)->m=p.
-Proof.
-Intro n; Pattern n; Apply Nind; Clear n; Simpl.
-  Trivial.
-  Intros n IHn m p H0; Do 2 Rewrite Nplus_succ in H0.
-  Apply IHn; Apply Nsucc_inj; Assumption.
-Qed.
-
-(** Properties of multiplication *)
-
-Theorem Nmult_1_l : (n:entier)(Nmult (Pos xH) n)=n.
-Proof.
-NewDestruct n; Reflexivity.
-Qed.
-
-Theorem Nmult_1_r : (n:entier)(Nmult n (Pos xH))=n.
-Proof.
-NewDestruct n; Simpl; Try Reflexivity.
-Rewrite times_x_1; Reflexivity.
-Qed.
-
-Theorem Nmult_comm : (n,m:entier)(Nmult n m)=(Nmult m n).
-Proof.
-Intros.
-NewDestruct n; NewDestruct m; Simpl; Try Reflexivity.
-Rewrite times_sym; Reflexivity.
-Qed.
-
-Theorem Nmult_assoc : 
-  (n,m,p:entier)(Nmult n (Nmult m p))=(Nmult (Nmult n m) p).
-Proof.
-Intros.
-NewDestruct n; Try Reflexivity.
-NewDestruct m; Try Reflexivity.
-NewDestruct p; Try Reflexivity.
-Simpl; Rewrite times_assoc; Reflexivity.
-Qed.
-
-Theorem Nmult_plus_distr_r :
-  (n,m,p:entier)(Nmult (Nplus n m) p)=(Nplus (Nmult n p) (Nmult m p)).
-Proof.
-Intros.
-NewDestruct n; Try Reflexivity.
-NewDestruct m; NewDestruct p; Try Reflexivity.
-Simpl; Rewrite times_add_distr_l; Reflexivity.
-Qed.
-
-Theorem Nmult_reg_r : (n,m,p:entier) ~p=Nul->(Nmult n p)=(Nmult m p) -> n=m.
-Proof.
-NewDestruct p; Intros Hp H.
-Contradiction Hp; Reflexivity.
-NewDestruct n; NewDestruct m; Reflexivity Orelse Try Discriminate H.
-Injection H; Clear H; Intro H; Rewrite simpl_times_r with 1:=H; Reflexivity.
-Qed. 
-
-Theorem Nmult_0_l : (n:entier) (Nmult Nul n) = Nul.
-Proof.
-Reflexivity.
-Qed.
-
-(** Properties of comparison *)
-
-Theorem Ncompare_Eq_eq : (n,m:entier) (Ncompare n m) = EGAL -> n = m.
-Proof.
-NewDestruct n as [|n]; NewDestruct m as [|m]; Simpl; Intro H;
-  Reflexivity Orelse Try Discriminate H.
-  Rewrite (compare_convert_EGAL n m H); Reflexivity.
-Qed.
-