O. M. G. The typechecking is much slower for this than all my previous proofs, and until I removed a bunch of cruft it overloaded the garbage collector.
I am now so much closer to proving my binary gcd implementation correct without leaving a certain lemma unproven. This is an obsession akin to the one that resulted in Sorts Mill Goudy (yes, the one that exists as a Google Font, thus the tie-in to Google+). I had no particular desire for a Goudy font, but I had a compulsion to make one.
(The compulsion did not extend to doing a boldface. I dislike boldface and think it usually better avoided entirely. Dictionaries are an exception; I prefer dictionaries that use boldface nicely.)