The Coq mailing list

[roux cody <cody.roux AT gmail.com>]

It reminds me of the old math joke, which I re-discovered here: http://math.stackexchange.com/questions/151782/when-is-something-obvious

"A famous maths professor was giving a lecture during which he said "it is obvious that..." and then he paused at length in thought, and then excused himself from the lecture temporarily. Upon his return some fifteen minutes later he said "Yes, it is obvious that...." and continued the lecture."

Best,

Cody

On Mon, Aug 8, 2016 at 5:12 PM, Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr> wrote:

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/