By Daniel Britten - supervised by Cristian S. Calude - and with guidance from Monica Marcus.
Source code for an honours dissertation at the University of Auckland. Available as a Centre for Discrete Mathematics and Theoretical Computer Science research report here: https://www.cs.auckland.ac.nz/research/groups/CDMTCS/researchreports/view-publication.php?selected-id=679
In order to interactively step through the proofs in this dissertation, CoqIde can be downloaded from https://coq.inria.fr/download.