Library Coq.Arith.Mult
Require Export Plus.
Require Export Minus.
Require Export Lt.
Require Export Le.
Open Local Scope nat_scope.
Implicit Types m n p :
nat.
Theorems about multiplication in nat. mult is defined in module Init/Peano.v.
Lemma mult_is_O :
forall n m,
n *
m = 0 ->
n = 0 \/
m = 0.
Lemma mult_is_one :
forall n m,
n *
m = 1 ->
n = 1 /\
m = 1.
Multiplication and successor
Compatibility with orders
n|->2*n and n|->2n+1 have disjoint image
tail_mult is an alternative definition for mult which is
tail-recursive, whereas mult is not. This can be useful
when extracting programs.
TailSimpl transforms any tail_plus and tail_mult into plus
and mult and simplify