The Coq mailing list

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

Just for fun, not asking anything.

I have been translating a proof of a certain theorem in Coq. Reading
the pen-and-paper proof, which is enough detailed, it is written:

   Iterating these, it is easy to see that...

I have been in this "it is easy" since several days... Well, I think
that I am going to find a solution, but in the meantime...

Fortunately, it is easy. What would it be if it was difficult?

And mathematicians don't like when we say that mathematical books and
papers are just litterature... :-)

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