The Coq mailing list

["Gyesik Lee" <leegy AT lix.polytechnique.fr>]

Hi,

I want to just summarize what the others have already said. 

a) Proofs of inductive properties are finite (or to be precise,
well-founded) and this is reflected in the associatedinduction
principle.

b) First you may have to show something by induction which is very
characteristic for the inductive definition. And then you can use it to
prove that something else cannot be true. Such cases occur often.

Best regards,

Gyesik