diff options
| -rw-r--r-- | theories/Arith/Mult.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index 507d956e81..d7f703e6e4 100644 --- a/theories/Arith/Mult.v +++ b/theories/Arith/Mult.v @@ -158,7 +158,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 [| n IHn]; simpl; auto. + intro n; induction n as [| n IHn]; simpl; auto. intros. rewrite Nat.add_assoc, IHn. f_equal. rewrite Nat.add_comm. apply plus_tail_plus. Qed. |