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

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

SearchRewrite (plus _ (S _)).