Idris2Doc
: Control.Permutation.Proofs
Index
Default
Alternative
Black & White
Control.Permutation.Proofs
factorialIncr
: (n :
Nat
) ->
LTE
(
factorial
n) (
factorial
(
S
n))
Proof that (n + 1)! >= n!
factorialLTE
: (n :
Nat
) ->
LTE
1
(
factorial
n)
Proof that n! >= 1