diff options
Diffstat (limited to 'theories')
| -rwxr-xr-x | theories/Arith/Arith.v | 1 | ||||
| -rw-r--r-- | theories/Arith/Factorial.v | 34 |
2 files changed, 35 insertions, 0 deletions
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. + |