summaryrefslogtreecommitdiff
path: root/theories/Numbers/NatInt/NZMul.v
blob: 14981a220533e4bfb949486730fe570048a1e99d (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
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)
(*                      Evgeny Makarov, INRIA, 2007                     *)
(************************************************************************)

(*i $Id$ i*)

Require Import NZAxioms NZBase NZAdd.

Module Type NZMulPropSig
 (Import NZ : NZAxiomsSig')(Import NZBase : NZBasePropSig NZ).
Include NZAddPropSig NZ NZBase.

Theorem mul_0_r : forall n, n * 0 == 0.
Proof.
nzinduct n; intros; now nzsimpl.
Qed.

Theorem mul_succ_r : forall n m, n * (S m) == n * m + n.
Proof.
intros n m; nzinduct n. now nzsimpl.
intro n. nzsimpl. rewrite succ_inj_wd, <- add_assoc, (add_comm m n), add_assoc.
now rewrite add_cancel_r.
Qed.

Hint Rewrite mul_0_r mul_succ_r : nz.

Theorem mul_comm : forall n m, n * m == m * n.
Proof.
intros n m; nzinduct n. now nzsimpl.
intro. nzsimpl. now rewrite add_cancel_r.
Qed.

Theorem mul_add_distr_r : forall n m p, (n + m) * p == n * p + m * p.
Proof.
intros n m p; nzinduct n. now nzsimpl.
intro n. nzsimpl. rewrite <- add_assoc, (add_comm p (m*p)), add_assoc.
now rewrite add_cancel_r.
Qed.

Theorem mul_add_distr_l : forall n m p, n * (m + p) == n * m + n * p.
Proof.
intros n m p.
rewrite (mul_comm n (m + p)), (mul_comm n m), (mul_comm n p).
apply mul_add_distr_r.
Qed.

Theorem mul_assoc : forall n m p, n * (m * p) == (n * m) * p.
Proof.
intros n m p; nzinduct n. now nzsimpl.
intro n. nzsimpl. rewrite mul_add_distr_r.
now rewrite add_cancel_r.
Qed.

Theorem mul_1_l : forall n, 1 * n == n.
Proof.
intro n. now nzsimpl.
Qed.

Theorem mul_1_r : forall n, n * 1 == n.
Proof.
intro n. now nzsimpl.
Qed.

End NZMulPropSig.