diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /theories/Arith/Factorial.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'theories/Arith/Factorial.v')
-rw-r--r-- | theories/Arith/Factorial.v | 29 |
1 files changed, 9 insertions, 20 deletions
diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v index 870ea4e1..7d29f23c 100644 --- a/theories/Arith/Factorial.v +++ b/theories/Arith/Factorial.v @@ -1,14 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Plus. -Require Import Mult. -Require Import Lt. +Require Import PeanoNat Plus Mult Lt. Local Open Scope nat_scope. (** Factorial *) @@ -21,28 +19,19 @@ Fixpoint fact (n:nat) : nat := Arguments fact n%nat. -Lemma lt_O_fact : forall n:nat, 0 < fact n. +Lemma lt_O_fact n : 0 < fact n. Proof. - simple induction n; unfold lt; simpl; auto with arith. + induction n; simpl; auto with arith. Qed. -Lemma fact_neq_0 : forall n:nat, fact n <> 0. +Lemma fact_neq_0 n : fact n <> 0. Proof. - intro. - apply not_eq_sym. - apply lt_O_neq. - apply lt_O_fact. + apply Nat.neq_0_lt_0, lt_O_fact. Qed. -Lemma fact_le : forall n m:nat, n <= m -> fact n <= fact m. +Lemma fact_le n m : 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. + - apply le_n. + - simpl. transitivity (fact m). trivial. apply Nat.le_add_r. Qed. |