Comment by bnegreve

Would it be possible to use proof assistants like Coq [1] to verify this kind of proofs ? If not, does anyone know why ?

[1] http://en.wikipedia.org/wiki/Coq