Ferreira JF.? 2010.??Designing an Algorithmic Proof of the Two-Squares Theorem. Mathematics of Program Construction (LNCS 6120).