The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Z wrote:
> Apparently it makes no difference to put or not put an  "intros n"
> before "induction n"
> Is this affirmation right?
>    

My answer is "pedantic No, normal Yes." :)

If the conclusion starts with [forall n], then your statement is right.  
[induction] automatically does [intros] up to the variable you name, so 
it matters that the variable is called [n] if you just start with 
[induction n].

If the conclusion started with [forall m], then [induction n] would 
fail, while [intros n; induction n] would do what you want.

P.S.: A friendly prodding: This is explained in the first few paragraphs 
of the Coq manual's section on [induction].