The Coq mailing list

[Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>]

Hi Petar,

On Sun, Dec 12, 2010 at 06:48:31PM +0100, Petar Maksimovic wrote:

> You could actually prove directly that your sum function is always
> equal to 'plus' on natural numbers. From this, you'll have no problem
> proving your lemma.

Thanks! I managed to change your proof not using Arith_base (looking
at the lemma you used) and expanding the 'auto' (I don't want to use
'auto' because I want to learn by understanding what happens). It works.

Well. But since I would like not to refer to 'plus', I am looking
now at Martijn and Stéphane's solutions.

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/