Start a tutorial about simple inductive types

[Villetaneuse]

Still a draft, but comments welcome, here is the plan:

• enumerated types
• inductive types with non inductive constructors
• nat (first example of an inductive inductive)
• positive (first example with two inductive constructors)
• lists (parameterized inductive)
• binary trees (first example with a constructor with 2 arguments of the inductive type)

Maybe that's too much.
Tactics are:

• discriminate
• destruct
• injection
• induction and we define functions with (simple) match

Maybe lists and binary trees could go in a separate tutorial?