, Lemma 1 Ltd. & Department of Computer Science, Oxford University

• Journal of Formalized Reasoning Vol. 9 No. 1 (2016): Special Issue: Twenty Years of the QED Manifesto - QED 20th anniversary
  Now f is continuous (exercise!)
  Abstract  PDF