Nouveaux lemmes (sur proposition de Nijmegen)

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

5 files changed, 46 insertions, 7 deletions

diff --git a/.depend.coq b/.depend.coq
index c4fae47594..7b691e16ea 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -53,18 +53,19 @@ theories/Reals/RiemannInt_SF.vo: theories/Reals/RiemannInt_SF.v theories/Reals/R
 theories/Reals/RiemannInt.vo: theories/Reals/RiemannInt.v theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis.vo theories/Reals/Rbase.vo theories/Reals/RiemannInt_SF.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo theories/Arith/Max.vo
 theories/Reals/Integration.vo: theories/Reals/Integration.v theories/Reals/NewtonInt.vo theories/Reals/RiemannInt_SF.vo theories/Reals/RiemannInt.vo
 theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo theories/Reals/Integration.vo
+theories/Init/Notations.vo: theories/Init/Notations.v
 theories/Init/Datatypes.vo: theories/Init/Datatypes.v
 theories/Init/DatatypesSyntax.vo: theories/Init/DatatypesSyntax.v
 theories/Init/Peano.vo: theories/Init/Peano.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Datatypes.vo
 theories/Init/PeanoSyntax.vo: theories/Init/PeanoSyntax.v theories/Init/Datatypes.vo theories/Init/Peano.vo
-theories/Init/Logic.vo: theories/Init/Logic.v theories/Init/Datatypes.vo
+theories/Init/Logic.vo: theories/Init/Logic.v theories/Init/Notations.vo theories/Init/Datatypes.vo
 theories/Init/Specif.vo: theories/Init/Specif.v theories/Init/Datatypes.vo theories/Init/Logic.vo theories/Init/LogicSyntax.vo
 theories/Init/LogicSyntax.vo: theories/Init/LogicSyntax.v theories/Init/Logic.vo
 theories/Init/SpecifSyntax.vo: theories/Init/SpecifSyntax.v theories/Init/Datatypes.vo theories/Init/Specif.vo
 theories/Init/Logic_Type.vo: theories/Init/Logic_Type.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo
 theories/Init/Wf.vo: theories/Init/Wf.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo
 theories/Init/Logic_TypeSyntax.vo: theories/Init/Logic_TypeSyntax.v theories/Init/Logic_Type.vo
-theories/Init/Prelude.vo: theories/Init/Prelude.v theories/Init/Datatypes.vo theories/Init/DatatypesSyntax.vo theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Specif.vo theories/Init/SpecifSyntax.vo theories/Init/Peano.vo theories/Init/PeanoSyntax.vo theories/Init/Wf.vo
+theories/Init/Prelude.vo: theories/Init/Prelude.v theories/Init/Notations.vo theories/Init/Datatypes.vo theories/Init/DatatypesSyntax.vo theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Specif.vo theories/Init/SpecifSyntax.vo theories/Init/Peano.vo theories/Init/PeanoSyntax.vo theories/Init/Wf.vo
 theories/Logic/Hurkens.vo: theories/Logic/Hurkens.v
 theories/Logic/ProofIrrelevance.vo: theories/Logic/ProofIrrelevance.v theories/Logic/Hurkens.vo
 theories/Logic/Classical.vo: theories/Logic/Classical.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Set.vo
@@ -79,7 +80,7 @@ theories/Logic/Berardi.vo: theories/Logic/Berardi.v
 theories/Logic/Eqdep_dec.vo: theories/Logic/Eqdep_dec.v
 theories/Logic/Decidable.vo: theories/Logic/Decidable.v
 theories/Logic/JMeq.vo: theories/Logic/JMeq.v theories/Logic/Eqdep.vo
-theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo
+theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo theories/Arith/Factorial.vo
 theories/Arith/Gt.vo: theories/Arith/Gt.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo
 theories/Arith/Between.vo: theories/Arith/Between.v theories/Arith/Le.vo theories/Arith/Lt.vo
 theories/Arith/Le.vo: theories/Arith/Le.v
@@ -98,6 +99,7 @@ theories/Arith/Plus.vo: theories/Arith/Plus.v theories/Arith/Le.vo theories/Arit
 theories/Arith/Wf_nat.vo: theories/Arith/Wf_nat.v theories/Arith/Lt.vo
 theories/Arith/Max.vo: theories/Arith/Max.v theories/Arith/Arith.vo
 theories/Arith/Bool_nat.vo: theories/Arith/Bool_nat.v theories/Arith/Compare_dec.vo theories/Arith/Peano_dec.vo theories/Bool/Sumbool.vo
+theories/Arith/Factorial.vo: theories/Arith/Factorial.v theories/Arith/Plus.vo theories/Arith/Lt.vo
 theories/Bool/Bool.vo: theories/Bool/Bool.v
 theories/Bool/IfProp.vo: theories/Bool/IfProp.v theories/Bool/Bool.vo
 theories/Bool/Zerob.vo: theories/Bool/Zerob.v theories/Arith/Arith.vo theories/Bool/Bool.vo
diff --git a/.depend.newcoq b/.depend.newcoq
index ff8fbc5d4c..823877947c 100644
--- a/.depend.newcoq
+++ b/.depend.newcoq
@@ -53,18 +53,19 @@ newtheories/Reals/RiemannInt_SF.vo: newtheories/Reals/RiemannInt_SF.v newtheorie
 newtheories/Reals/RiemannInt.vo: newtheories/Reals/RiemannInt.v newtheories/Reals/Rfunctions.vo newtheories/Reals/SeqSeries.vo newtheories/Reals/Ranalysis.vo newtheories/Reals/Rbase.vo newtheories/Reals/RiemannInt_SF.vo newtheories/Logic/Classical_Prop.vo newtheories/Logic/Classical_Pred_Type.vo newtheories/Arith/Max.vo
 newtheories/Reals/Integration.vo: newtheories/Reals/Integration.v newtheories/Reals/NewtonInt.vo newtheories/Reals/RiemannInt_SF.vo newtheories/Reals/RiemannInt.vo
 newtheories/Reals/Reals.vo: newtheories/Reals/Reals.v newtheories/Reals/Rbase.vo newtheories/Reals/Rfunctions.vo newtheories/Reals/SeqSeries.vo newtheories/Reals/Rtrigo.vo newtheories/Reals/Ranalysis.vo newtheories/Reals/Integration.vo
+newtheories/Init/Notations.vo: newtheories/Init/Notations.v
 newtheories/Init/Datatypes.vo: newtheories/Init/Datatypes.v
 newtheories/Init/DatatypesSyntax.vo: newtheories/Init/DatatypesSyntax.v
 newtheories/Init/Peano.vo: newtheories/Init/Peano.v newtheories/Init/Logic.vo newtheories/Init/LogicSyntax.vo newtheories/Init/Datatypes.vo
 newtheories/Init/PeanoSyntax.vo: newtheories/Init/PeanoSyntax.v newtheories/Init/Datatypes.vo newtheories/Init/Peano.vo
-newtheories/Init/Logic.vo: newtheories/Init/Logic.v newtheories/Init/Datatypes.vo
+newtheories/Init/Logic.vo: newtheories/Init/Logic.v newtheories/Init/Notations.vo newtheories/Init/Datatypes.vo
 newtheories/Init/Specif.vo: newtheories/Init/Specif.v newtheories/Init/Datatypes.vo newtheories/Init/Logic.vo newtheories/Init/LogicSyntax.vo
 newtheories/Init/LogicSyntax.vo: newtheories/Init/LogicSyntax.v newtheories/Init/Logic.vo
 newtheories/Init/SpecifSyntax.vo: newtheories/Init/SpecifSyntax.v newtheories/Init/Datatypes.vo newtheories/Init/Specif.vo
 newtheories/Init/Logic_Type.vo: newtheories/Init/Logic_Type.v newtheories/Init/Logic.vo newtheories/Init/LogicSyntax.vo
 newtheories/Init/Wf.vo: newtheories/Init/Wf.v newtheories/Init/Logic.vo newtheories/Init/LogicSyntax.vo
 newtheories/Init/Logic_TypeSyntax.vo: newtheories/Init/Logic_TypeSyntax.v newtheories/Init/Logic_Type.vo
-newtheories/Init/Prelude.vo: newtheories/Init/Prelude.v newtheories/Init/Datatypes.vo newtheories/Init/DatatypesSyntax.vo newtheories/Init/Logic.vo newtheories/Init/LogicSyntax.vo newtheories/Init/Specif.vo newtheories/Init/SpecifSyntax.vo newtheories/Init/Peano.vo newtheories/Init/PeanoSyntax.vo newtheories/Init/Wf.vo
+newtheories/Init/Prelude.vo: newtheories/Init/Prelude.v newtheories/Init/Notations.vo newtheories/Init/Datatypes.vo newtheories/Init/DatatypesSyntax.vo newtheories/Init/Logic.vo newtheories/Init/LogicSyntax.vo newtheories/Init/Specif.vo newtheories/Init/SpecifSyntax.vo newtheories/Init/Peano.vo newtheories/Init/PeanoSyntax.vo newtheories/Init/Wf.vo
 newtheories/Logic/Hurkens.vo: newtheories/Logic/Hurkens.v
 newtheories/Logic/ProofIrrelevance.vo: newtheories/Logic/ProofIrrelevance.v newtheories/Logic/Hurkens.vo
 newtheories/Logic/Classical.vo: newtheories/Logic/Classical.v newtheories/Logic/Classical_Prop.vo newtheories/Logic/Classical_Pred_Set.vo
@@ -79,7 +80,7 @@ newtheories/Logic/Berardi.vo: newtheories/Logic/Berardi.v
 newtheories/Logic/Eqdep_dec.vo: newtheories/Logic/Eqdep_dec.v
 newtheories/Logic/Decidable.vo: newtheories/Logic/Decidable.v
 newtheories/Logic/JMeq.vo: newtheories/Logic/JMeq.v newtheories/Logic/Eqdep.vo
-newtheories/Arith/Arith.vo: newtheories/Arith/Arith.v newtheories/Arith/Le.vo newtheories/Arith/Lt.vo newtheories/Arith/Plus.vo newtheories/Arith/Gt.vo newtheories/Arith/Minus.vo newtheories/Arith/Mult.vo newtheories/Arith/Between.vo newtheories/Arith/Peano_dec.vo newtheories/Arith/Compare_dec.vo
+newtheories/Arith/Arith.vo: newtheories/Arith/Arith.v newtheories/Arith/Le.vo newtheories/Arith/Lt.vo newtheories/Arith/Plus.vo newtheories/Arith/Gt.vo newtheories/Arith/Minus.vo newtheories/Arith/Mult.vo newtheories/Arith/Between.vo newtheories/Arith/Peano_dec.vo newtheories/Arith/Compare_dec.vo newtheories/Arith/Factorial.vo
 newtheories/Arith/Gt.vo: newtheories/Arith/Gt.v newtheories/Arith/Le.vo newtheories/Arith/Lt.vo newtheories/Arith/Plus.vo
 newtheories/Arith/Between.vo: newtheories/Arith/Between.v newtheories/Arith/Le.vo newtheories/Arith/Lt.vo
 newtheories/Arith/Le.vo: newtheories/Arith/Le.v
@@ -98,6 +99,7 @@ newtheories/Arith/Plus.vo: newtheories/Arith/Plus.v newtheories/Arith/Le.vo newt
 newtheories/Arith/Wf_nat.vo: newtheories/Arith/Wf_nat.v newtheories/Arith/Lt.vo
 newtheories/Arith/Max.vo: newtheories/Arith/Max.v newtheories/Arith/Arith.vo
 newtheories/Arith/Bool_nat.vo: newtheories/Arith/Bool_nat.v newtheories/Arith/Compare_dec.vo newtheories/Arith/Peano_dec.vo newtheories/Bool/Sumbool.vo
+newtheories/Arith/Factorial.vo: newtheories/Arith/Factorial.v newtheories/Arith/Plus.vo newtheories/Arith/Lt.vo
 newtheories/Bool/Bool.vo: newtheories/Bool/Bool.v
 newtheories/Bool/IfProp.vo: newtheories/Bool/IfProp.v newtheories/Bool/Bool.vo
 newtheories/Bool/Zerob.vo: newtheories/Bool/Zerob.v newtheories/Arith/Arith.vo newtheories/Bool/Bool.vo
diff --git a/Makefile b/Makefile
index 412de905f0..1dbb7ac47a 100644
--- a/Makefile
+++ b/Makefile
@@ -548,7 +548,7 @@ ARITHVO=theories/Arith/Arith.vo         theories/Arith/Gt.vo          \
 	theories/Arith/EqNat.vo         theories/Arith/Peano_dec.vo   \
 	theories/Arith/Euclid.vo        theories/Arith/Plus.vo        \
 	theories/Arith/Wf_nat.vo  	theories/Arith/Max.vo	      \
-	theories/Arith/Bool_nat.vo
+	theories/Arith/Bool_nat.vo	theories/Arith/Factorial.vo   \
 #	theories/Arith/Div.vo 
 
 SORTINGVO=theories/Sorting/Heap.vo \
diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v
index 13c17aabb5..832ea7a427 100755
--- a/theories/Arith/Arith.v
+++ b/theories/Arith/Arith.v
@@ -18,3 +18,4 @@ Require Export Between.
 Require Export Minus.
 Require Export Peano_dec.
 Require Export Compare_dec.
+Require Export Factorial.
diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v
new file mode 100644
index 0000000000..4963379e68
--- /dev/null
+++ b/theories/Arith/Factorial.v
@@ -0,0 +1,34 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+Require Plus.
+Require Lt.
+
+(** Factorial *)
+
+Fixpoint fact [n:nat]:nat:=
+  Cases n of
+     O     => (S O)
+    |(S n) => (mult (S n) (fact n))
+  end.
+
+Lemma lt_O_fact : (n:nat)(lt O (fact n)).
+Proof.
+Induction n; Unfold lt; Simpl; Auto with arith.
+Qed.
+
+Lemma fact_neq_0:(n:nat)~(fact n)=O.
+Proof.
+Intro.
+Apply sym_not_eq.
+Apply lt_O_neq.
+Apply lt_O_fact.
+Qed.
+