blob: a8a60c983659058a7077c97e39a9ca8ae5ec4973 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: Factorial.v,v 1.1.2.1 2004/07/16 19:31:24 herbelin Exp $ i*)
Require Plus.
Require Mult.
Require Lt.
V7only [Import nat_scope.].
Open Local Scope nat_scope.
(** Factorial *)
Fixpoint fact [n:nat]:nat:=
Cases n of
O => (S O)
|(S n) => (mult (S n) (fact n))
end.
Arguments Scope fact [ nat_scope ].
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.
Lemma fact_growing : (n,m:nat) (le n m) -> (le (fact n) (fact m)).
Proof.
NewInduction 1.
Apply le_n.
Assert (le (mult (S O) (fact n)) (mult (S m) (fact m))).
Apply le_mult_mult.
Apply lt_le_S; Apply lt_O_Sn.
Assumption.
Simpl (mult (S O) (fact n)) in H0.
Rewrite <- plus_n_O in H0.
Assumption.
Qed.
|
