This is an unofficial reimagining of the Archive of Formal Proofs
Binary Heaps for IMP2by Simon Griebel