Library Coq.Numbers.Natural.Abstract.NMul
Theorems that are valid for both natural numbers and integers
Theorem mul_0_r :
forall n,
n * 0 == 0.
Theorem mul_succ_r :
forall n m,
n * (
S m) ==
n *
m +
n.
Theorem mul_comm :
forall n m :
N,
n *
m ==
m *
n.
Theorem mul_add_distr_r :
forall n m p :
N, (
n +
m) *
p ==
n *
p +
m *
p.
Theorem mul_add_distr_l :
forall n m p :
N,
n * (
m +
p) ==
n *
m +
n *
p.
Theorem mul_assoc :
forall n m p :
N,
n * (
m *
p) == (
n *
m) *
p.
Theorem mul_1_l :
forall n :
N, 1 *
n ==
n.
Theorem mul_1_r :
forall n :
N,
n * 1 ==
n.
Theorem add_mul_repl_pair :
forall a n m n' m' u v :
N,
a *
n +
u ==
a *
m +
v ->
n +
m' ==
n' +
m ->
a *
n' +
u ==
a *
m' +
v.
End NMulPropFunct.