Proof by computation in the Coq system
scientific article; zbMATH DE number 1715300