diff options
| -rw-r--r-- | theories/Arith/Plus.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v index ec7426e648..5da7738adc 100644 --- a/theories/Arith/Plus.v +++ b/theories/Arith/Plus.v @@ -156,7 +156,7 @@ Fixpoint tail_plus n m : nat := Lemma plus_tail_plus : forall n m, n + m = tail_plus n m. Proof. -induction n as [| n IHn]; simpl; auto. +intro n; induction n as [| n IHn]; simpl; auto. intro m; rewrite <- IHn; simpl; auto. Qed. |