diff options
| author | coqbot-app[bot] | 2020-09-29 09:02:05 +0000 |
|---|---|---|
| committer | GitHub | 2020-09-29 09:02:05 +0000 |
| commit | ff74bba7c4ef0c6f3e17944b015e05fc23bad1af (patch) | |
| tree | 4d7ccf4a2eaf50ba4156f5a8040188c649efe893 /theories/Arith/Mult.v | |
| parent | 982c28216f3eb49abfd6b97c69b8fc116c813117 (diff) | |
| parent | cc4494897f0897f5795c2bd25fc06d4b07c73667 (diff) | |
Merge PR #13039: Lint stdlib with -mangle-names #3
Reviewed-by: anton-trunov
Diffstat (limited to 'theories/Arith/Mult.v')
| -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. |