Library Coq.Arith.Factorial
Require
Import
Plus
.
Require
Import
Mult
.
Require
Import
Lt
.
Open
Local
Scope
nat_scope
.
Factorial
Boxed
Fixpoint
fact
(
n
:nat) :
nat
:=
match
n
with
|
O
=> 1
|
S
n
=>
S
n
*
fact
n
end
.
Lemma
lt_O_fact
:
forall
n
:nat, 0 <
fact
n
.
Lemma
fact_neq_0
:
forall
n
:nat,
fact
n
<> 0.
Lemma
fact_le
:
forall
n
m
:nat,
n
<=
m
->
fact
n
<=
fact
m
.