diff options
author | 2006-10-17 12:53:34 +0000 | |
---|---|---|
committer | 2006-10-17 12:53:34 +0000 | |
commit | 28dc7a05cc1d3e03ed1435b3db4340db954a59e2 (patch) | |
tree | 63cdf18cd47260eb90550f62f7b22e2e2e208f6c /theories/Arith/Factorial.v | |
parent | 744e7f6a319f4d459a3cc2309f575d43041d75aa (diff) |
Mise en forme des theories
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Arith/Factorial.v')
-rw-r--r-- | theories/Arith/Factorial.v | 32 |
1 files changed, 16 insertions, 16 deletions
diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v index 9f7de8503..8c5315624 100644 --- a/theories/Arith/Factorial.v +++ b/theories/Arith/Factorial.v @@ -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. |