diff options
Diffstat (limited to 'theories/Arith/Mult.v')
-rw-r--r-- | theories/Arith/Mult.v | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index 64b0d4dd3..0c44cfaf1 100644 --- a/theories/Arith/Mult.v +++ b/theories/Arith/Mult.v @@ -23,7 +23,7 @@ Implicit Types m n p : nat. Lemma mult_0_r : forall n, n * 0 = 0. Proof. - intro; symmetry in |- *; apply mult_n_O. + intro; symmetry ; apply mult_n_O. Qed. Lemma mult_0_l : forall n, 0 * n = 0. @@ -35,7 +35,7 @@ Qed. Lemma mult_1_l : forall n, 1 * n = n. Proof. - simpl in |- *; auto with arith. + simpl; auto with arith. Qed. Hint Resolve mult_1_l: arith v62. @@ -68,7 +68,7 @@ Hint Resolve mult_plus_distr_r: arith v62. Lemma mult_plus_distr_l : forall n m p, n * (m + p) = n * m + n * p. Proof. induction n. trivial. - intros. simpl in |- *. rewrite IHn. symmetry. apply plus_permute_2_in_4. + intros. simpl. rewrite IHn. symmetry. apply plus_permute_2_in_4. Qed. Lemma mult_minus_distr_r : forall n m p, (n - m) * p = n * p - m * p. @@ -137,13 +137,13 @@ Qed. Lemma mult_O_le : forall n m, m = 0 \/ n <= m * n. Proof. - induction m; simpl in |- *; auto with arith. + induction m; simpl; auto with arith. Qed. Hint Resolve mult_O_le: arith v62. Lemma mult_le_compat_l : forall n m p, n <= m -> p * n <= p * m. Proof. - induction p as [| p IHp]; intros; simpl in |- *. + induction p as [| p IHp]; intros; simpl. apply le_n. auto using plus_le_compat. Qed. @@ -167,7 +167,7 @@ Proof. assumption. apply le_plus_l. (* m*p<=m0*q -> m*p<=(S m0)*q *) - simpl in |- *; apply le_trans with (m0 * q). + simpl; apply le_trans with (m0 * q). assumption. apply le_plus_r. Qed. @@ -232,7 +232,7 @@ Fixpoint mult_acc (s:nat) m n : nat := Lemma mult_acc_aux : forall n m p, m + n * p = mult_acc m p n. Proof. - induction n as [| p IHp]; simpl in |- *; auto. + induction n as [| p IHp]; simpl; auto. intros s m; rewrite <- plus_tail_plus; rewrite <- IHp. rewrite <- plus_assoc_reverse; apply f_equal2; auto. rewrite plus_comm; auto. @@ -242,7 +242,7 @@ Definition tail_mult n m := mult_acc 0 m n. Lemma mult_tail_mult : forall n m, n * m = tail_mult n m. Proof. - intros; unfold tail_mult in |- *; rewrite <- mult_acc_aux; auto. + intros; unfold tail_mult; rewrite <- mult_acc_aux; auto. Qed. (** [TailSimpl] transforms any [tail_plus] and [tail_mult] into [plus] @@ -250,4 +250,4 @@ Qed. Ltac tail_simpl := repeat rewrite <- plus_tail_plus; repeat rewrite <- mult_tail_mult; - simpl in |- *. + simpl. |