blob: fda8b7a34bb6dfb47265aa80051afadb7cd72d4f (
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
71
72
73
74
75
76
77
78
79
80
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
(*i $Id: NZMul.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
Require Import NZAxioms.
Require Import NZAdd.
Module NZMulPropFunct (Import NZAxiomsMod : NZAxiomsSig).
Module Export NZAddPropMod := NZAddPropFunct NZAxiomsMod.
Open Local Scope NatIntScope.
Theorem NZmul_0_r : forall n : NZ, n * 0 == 0.
Proof.
NZinduct n.
now rewrite NZmul_0_l.
intro. rewrite NZmul_succ_l. now rewrite NZadd_0_r.
Qed.
Theorem NZmul_succ_r : forall n m : NZ, n * (S m) == n * m + n.
Proof.
intros n m; NZinduct n.
do 2 rewrite NZmul_0_l; now rewrite NZadd_0_l.
intro n. do 2 rewrite NZmul_succ_l. do 2 rewrite NZadd_succ_r.
rewrite NZsucc_inj_wd. rewrite <- (NZadd_assoc (n * m) m n).
rewrite (NZadd_comm m n). rewrite NZadd_assoc.
now rewrite NZadd_cancel_r.
Qed.
Theorem NZmul_comm : forall n m : NZ, n * m == m * n.
Proof.
intros n m; NZinduct n.
rewrite NZmul_0_l; now rewrite NZmul_0_r.
intro. rewrite NZmul_succ_l; rewrite NZmul_succ_r. now rewrite NZadd_cancel_r.
Qed.
Theorem NZmul_add_distr_r : forall n m p : NZ, (n + m) * p == n * p + m * p.
Proof.
intros n m p; NZinduct n.
rewrite NZmul_0_l. now do 2 rewrite NZadd_0_l.
intro n. rewrite NZadd_succ_l. do 2 rewrite NZmul_succ_l.
rewrite <- (NZadd_assoc (n * p) p (m * p)).
rewrite (NZadd_comm p (m * p)). rewrite (NZadd_assoc (n * p) (m * p) p).
now rewrite NZadd_cancel_r.
Qed.
Theorem NZmul_add_distr_l : forall n m p : NZ, n * (m + p) == n * m + n * p.
Proof.
intros n m p.
rewrite (NZmul_comm n (m + p)). rewrite (NZmul_comm n m).
rewrite (NZmul_comm n p). apply NZmul_add_distr_r.
Qed.
Theorem NZmul_assoc : forall n m p : NZ, n * (m * p) == (n * m) * p.
Proof.
intros n m p; NZinduct n.
now do 3 rewrite NZmul_0_l.
intro n. do 2 rewrite NZmul_succ_l. rewrite NZmul_add_distr_r.
now rewrite NZadd_cancel_r.
Qed.
Theorem NZmul_1_l : forall n : NZ, 1 * n == n.
Proof.
intro n. rewrite NZmul_succ_l; rewrite NZmul_0_l. now rewrite NZadd_0_l.
Qed.
Theorem NZmul_1_r : forall n : NZ, n * 1 == n.
Proof.
intro n; rewrite NZmul_comm; apply NZmul_1_l.
Qed.
End NZMulPropFunct.
|
