glguy's binary numbers with some extra stuff
Some proofs and reorganization of Eric Mertens' modularfin module for Agda.