The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

> Here is a possible proof

Just a bit of advertising for SMTCoq (it can be installed via opam if 
you have extra dev):
it allows to safely called  the Smt solver veriT 
(http://www.verit-solver.org/) by checking its traces.

So if you have SMTcoq and veriT on your machine, the puzzle is proved 
automatically in 1 second!

--
Laurent

Attachment: puzzle_verity.v
Description: application/coq