diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-28 20:06:42 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-28 20:06:42 +0000 |
commit | 1f195b9b69b12ace9152b5fc815417f29fe54245 (patch) | |
tree | 9833fddeae2867fea4cbbc52df7773a22ae28af0 /theories/Arith/Mult.v | |
parent | 133ce76b38344b062699cc418e59d400becf27b4 (diff) |
- Modification de la déf de minus et pred conformément aux remarques de
Assia et Benjamin W. de telle sorte qu'ils respectent le critère de
décroissance structurelle lorsqu'utilisés dans un point-fixe.
- Ajout des noms "standard" des lemmes de Peano et correction d'un nom de
BinInt.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11015 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Arith/Mult.v')
-rw-r--r-- | theories/Arith/Mult.v | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index 3c3f3a093..348034427 100644 --- a/theories/Arith/Mult.v +++ b/theories/Arith/Mult.v @@ -127,6 +127,20 @@ Proof. 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. @@ -246,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 |- *. |