A simple proof by induction

Consider the following function, which returns the double of its argument (of type nat). 
Require Arith.

Fixpoint mult2 (n:nat) : nat :=
  match n with
    O => O
  | (S p) => (S (S (mult2 p)))
  end.
Show that, for each n, (mult2 n) is equal to n+n.

Solution

Look at this file

Note

In order to simplify a term like (plus n0 (S n0)), first consult Coq's library by typing : 
SearchRewrite (plus _ (S _)).