# 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 _)).

Going home

Pierre Castéran