A tutorial on [co-]inductive types in coq

This document1 is an introduction to the definition and use of inductive and co-inductive types in the Coq proof environment. It explains how types like natural numbers and infinite streams are defined in Coq, and the kind of proof techniques that can be used to reason about them (case analysis, induc-tion, inversion of predicates, co-induction, etc). Each technique is illustrated through an executable and self-contained Coq script