diff options
Diffstat (limited to 'theories/Arith/Mult.v')
-rw-r--r-- | theories/Arith/Mult.v | 41 |
1 files changed, 39 insertions, 2 deletions
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index 2315e12c..a43579f9 100644 --- a/theories/Arith/Mult.v +++ b/theories/Arith/Mult.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Mult.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Mult.v 11015 2008-05-28 20:06:42Z herbelin $ i*) Require Export Plus. Require Export Minus. @@ -104,6 +104,43 @@ Proof. Qed. Hint Resolve mult_assoc: arith v62. +(** ** Inversion lemmas *) + +Lemma mult_is_O : forall n m, n * m = 0 -> n = 0 \/ m = 0. +Proof. + destruct n as [| n]. + intros; left; trivial. + + simpl; intros m H; right. + assert (H':m = 0 /\ n * m = 0) by apply (plus_is_O _ _ H). + destruct H'; trivial. +Qed. + +Lemma mult_is_one : forall n m, n * m = 1 -> n = 1 /\ m = 1. +Proof. + destruct n as [|n]. + simpl; intros m H; elim (O_S _ H). + + simpl; intros m H. + destruct (plus_is_one _ _ H) as [[Hm Hnm] | [Hm Hnm]]. + rewrite Hm in H; simpl in H; rewrite mult_0_r in H; elim (O_S _ H). + rewrite Hm in Hnm; rewrite mult_1_r in Hnm; auto. +Qed. + +(** ** Multiplication and successor *) + +Lemma mult_succ_l : forall n m:nat, S n * m = n * m + m. +Proof. + intros; simpl. rewrite plus_comm. reflexivity. +Qed. + +Lemma mult_succ_r : forall n m:nat, n * S m = n * m + n. +Proof. + induction n as [| p H]; intro m; simpl. + reflexivity. + rewrite H, <- plus_n_Sm; apply f_equal; rewrite plus_assoc; reflexivity. +Qed. + (** * Compatibility with orders *) Lemma mult_O_le : forall n m, m = 0 \/ n <= m * n. @@ -223,4 +260,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 |- *. |