diff options
author | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-13 16:14:38 +0000 |
---|---|---|
committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-13 16:14:38 +0000 |
commit | 2f2715e8f4b1ecbee70c1463e5dde34dced3b2fb (patch) | |
tree | 562d072b17cc6c50a9ce842a0132df6f56123ef9 /theories/Arith/Mult.v | |
parent | e6c0a624ae7f766d5141649d85091cd3c056903b (diff) |
Ajout du théorème mult_minus_distr_l
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9237 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Arith/Mult.v')
-rw-r--r-- | theories/Arith/Mult.v | 29 |
1 files changed, 18 insertions, 11 deletions
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index 3e7d8454b..85977244e 100644 --- a/theories/Arith/Mult.v +++ b/theories/Arith/Mult.v @@ -29,6 +29,16 @@ Proof. reflexivity. Qed. +(** Commutativity *) + +Lemma mult_comm : forall n m, n * m = m * n. +Proof. +intros; elim n; intros; simpl in |- *; auto with arith. +elim mult_n_Sm. +elim H; apply plus_comm. +Qed. +Hint Resolve mult_comm: arith v62. + (** Distributivity *) Lemma mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p. @@ -52,6 +62,13 @@ elim minus_plus_simpl_l_reverse; auto with arith. Qed. Hint Resolve mult_minus_distr_r: arith v62. +Lemma mult_minus_distr_l : forall n m p, n * (m - p) = n * m - n * p. +Proof. + intros n m p. rewrite mult_comm. rewrite mult_minus_distr_r. + rewrite (mult_comm m n); rewrite (mult_comm p n); reflexivity. +Qed. +Hint Resolve mult_minus_distr_l: arith v62. + (** Associativity *) Lemma mult_assoc_reverse : forall n m p, n * m * p = n * (m * p). @@ -68,16 +85,6 @@ auto with arith. Qed. Hint Resolve mult_assoc: arith v62. -(** Commutativity *) - -Lemma mult_comm : forall n m, n * m = m * n. -Proof. -intros; elim n; intros; simpl in |- *; auto with arith. -elim mult_n_Sm. -elim H; apply plus_comm. -Qed. -Hint Resolve mult_comm: arith v62. - (** 1 is neutral *) Lemma mult_1_l : forall n, 1 * n = n. @@ -208,4 +215,4 @@ Qed. Ltac tail_simpl := repeat rewrite <- plus_tail_plus; repeat rewrite <- mult_tail_mult; - simpl in |- *.
\ No newline at end of file + simpl in |- *. |