diff options
author | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
tree | 591e9e512063e34099782e2518573f15ffeac003 /theories/Arith/Factorial.v | |
parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'theories/Arith/Factorial.v')
-rw-r--r-- | theories/Arith/Factorial.v | 34 |
1 files changed, 17 insertions, 17 deletions
diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v index 2767f9f0..5e2f491a 100644 --- a/theories/Arith/Factorial.v +++ b/theories/Arith/Factorial.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Factorial.v 6338 2004-11-22 09:10:51Z gregoire $ i*) +(*i $Id: Factorial.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Import Plus. Require Import Mult. @@ -17,34 +17,34 @@ Open Local Scope nat_scope. Boxed Fixpoint fact (n:nat) : nat := match n with - | O => 1 - | S n => S n * fact n + | O => 1 + | S n => S n * fact n end. Arguments Scope fact [nat_scope]. Lemma lt_O_fact : forall n:nat, 0 < fact n. Proof. -simple induction n; unfold lt in |- *; simpl in |- *; auto with arith. + simple induction n; unfold lt in |- *; simpl in |- *; auto with arith. Qed. Lemma fact_neq_0 : forall n:nat, fact n <> 0. Proof. -intro. -apply sym_not_eq. -apply lt_O_neq. -apply lt_O_fact. + intro. + apply sym_not_eq. + apply lt_O_neq. + apply lt_O_fact. Qed. Lemma fact_le : forall n m:nat, n <= m -> fact n <= fact m. Proof. -induction 1. -apply le_n. -assert (1 * fact n <= S m * fact m). -apply mult_le_compat. -apply lt_le_S; apply lt_O_Sn. -assumption. -simpl (1 * fact n) in H0. -rewrite <- plus_n_O in H0. -assumption. + induction 1. + apply le_n. + assert (1 * fact n <= S m * fact m). + apply mult_le_compat. + apply lt_le_S; apply lt_O_Sn. + assumption. + simpl (1 * fact n) in H0. + rewrite <- plus_n_O in H0. + assumption. Qed. |