From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- theories/Arith/Mult.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'theories/Arith/Mult.v') diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index 96581243..a173efc1 100644 --- a/theories/Arith/Mult.v +++ b/theories/Arith/Mult.v @@ -31,13 +31,13 @@ Notation mult_0_r := Nat.mul_0_r (compat "8.4"). (* n * 0 = 0 *) Notation mult_1_l := Nat.mul_1_l (compat "8.4"). (* 1 * n = n *) Notation mult_1_r := Nat.mul_1_r (compat "8.4"). (* n * 1 = n *) -Hint Resolve mult_1_l mult_1_r: arith v62. +Hint Resolve mult_1_l mult_1_r: arith. (** ** Commutativity *) Notation mult_comm := Nat.mul_comm (compat "8.4"). (* n * m = m * n *) -Hint Resolve mult_comm: arith v62. +Hint Resolve mult_comm: arith. (** ** Distributivity *) @@ -53,9 +53,9 @@ Notation mult_minus_distr_r := Notation mult_minus_distr_l := Nat.mul_sub_distr_l (compat "8.4"). (* n*(m-p) = n*m - n*p *) -Hint Resolve mult_plus_distr_r: arith v62. -Hint Resolve mult_minus_distr_r: arith v62. -Hint Resolve mult_minus_distr_l: arith v62. +Hint Resolve mult_plus_distr_r: arith. +Hint Resolve mult_minus_distr_r: arith. +Hint Resolve mult_minus_distr_l: arith. (** ** Associativity *) @@ -66,8 +66,8 @@ Proof. symmetry. apply Nat.mul_assoc. Qed. -Hint Resolve mult_assoc_reverse: arith v62. -Hint Resolve mult_assoc: arith v62. +Hint Resolve mult_assoc_reverse: arith. +Hint Resolve mult_assoc: arith. (** ** Inversion lemmas *) @@ -92,7 +92,7 @@ Lemma mult_O_le n m : m = 0 \/ n <= m * n. Proof. destruct m; [left|right]; simpl; trivial using Nat.le_add_r. Qed. -Hint Resolve mult_O_le: arith v62. +Hint Resolve mult_O_le: arith. Lemma mult_le_compat_l n m p : n <= m -> p * n <= p * m. Proof. -- cgit v1.2.3