A simple proof by induction
Consider the following function, which returns the double
of its argument (of type nat).
Fixpoint mult2 (n:nat) : nat :=
match n with
O => O
| (S p) => (S (S (mult2 p)))
Show that, for each n, (mult2 n)
is equal to n+n.
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 _)).