diff options
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. |