The Coq mailing list

[Martijn Vermaat <martijn AT vermaat.name>]

>   Fixpoint sum (a b : nat) : nat :=
>     match b with
>     | 0 => a
>     | S b1 => sum (S a) b1
>     end.
> 
>   Lemma sum_zero : forall a : nat, sum 0 a = a.


I think the most obvious way is by first proving the following fact:

  Lemma sum_S : forall a b : nat, sum a (S b) = S (sum a b).

From this it is actually quite easy to prove sum_zero.

cheers,
Martijn