diff options
Diffstat (limited to 'theories/Arith/Mult.v')
| -rw-r--r-- | theories/Arith/Mult.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index d7f703e6e4..584b282f4d 100644 --- a/theories/Arith/Mult.v +++ b/theories/Arith/Mult.v @@ -33,12 +33,14 @@ Notation mult_0_r := Nat.mul_0_r (only parsing). (* n * 0 = 0 *) Notation mult_1_l := Nat.mul_1_l (only parsing). (* 1 * n = n *) Notation mult_1_r := Nat.mul_1_r (only parsing). (* n * 1 = n *) +#[global] Hint Resolve mult_1_l mult_1_r: arith. (** ** Commutativity *) Notation mult_comm := Nat.mul_comm (only parsing). (* n * m = m * n *) +#[global] Hint Resolve mult_comm: arith. (** ** Distributivity *) @@ -55,8 +57,11 @@ Notation mult_minus_distr_r := Notation mult_minus_distr_l := Nat.mul_sub_distr_l (only parsing). (* n*(m-p) = n*m - n*p *) +#[global] Hint Resolve mult_plus_distr_r: arith. +#[global] Hint Resolve mult_minus_distr_r: arith. +#[global] Hint Resolve mult_minus_distr_l: arith. (** ** Associativity *) @@ -68,7 +73,9 @@ Proof. symmetry. apply Nat.mul_assoc. Qed. +#[global] Hint Resolve mult_assoc_reverse: arith. +#[global] Hint Resolve mult_assoc: arith. (** ** Inversion lemmas *) @@ -94,12 +101,14 @@ Lemma mult_O_le n m : m = 0 \/ n <= m * n. Proof. destruct m; [left|right]; simpl; trivial using Nat.le_add_r. Qed. +#[global] Hint Resolve mult_O_le: arith. Lemma mult_le_compat_l n m p : n <= m -> p * n <= p * m. Proof. apply Nat.mul_le_mono_nonneg_l, Nat.le_0_l. (* TODO : get rid of 0<=n hyp *) Qed. +#[global] Hint Resolve mult_le_compat_l: arith. Lemma mult_le_compat_r n m p : n <= m -> n * p <= m * p. @@ -117,6 +126,7 @@ Proof. apply Nat.mul_lt_mono_pos_l, Nat.lt_0_succ. Qed. +#[global] Hint Resolve mult_S_lt_compat_l: arith. Lemma mult_lt_compat_l n m p : n < m -> 0 < p -> p * n < p * m. |