Bingham, J. Formalizing a Proof That E Is Transcendental. JFR 2011, 4, 71-84.