diff options
author | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-30 09:27:30 +0000 |
---|---|---|
committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-30 09:27:30 +0000 |
commit | 67040519baa5b82495135a84ae1a79e45a1af42b (patch) | |
tree | 2172b90d4a95c594934968ae019c72865912a314 /theories/Arith/Mult.v | |
parent | 7fd5ade892dcb487cacc646335601dc3bc52009e (diff) |
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
Diffstat (limited to 'theories/Arith/Mult.v')
-rw-r--r-- | theories/Arith/Mult.v | 23 |
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. |