Ajout de lemmes d'inversion pour mult (sur le modèle de plus_is_O et plus_is_one)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10273 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 23 insertions, 0 deletions

diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index ab3e65856..386800934 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -104,6 +104,29 @@ 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.
+  induction n as [|n IH].
+    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.
+
 (** * Compatibility with orders *)
 
 Lemma mult_O_le : forall n m, m = 0 \/ n <= m * n.