1 2# Fermat's Two Squares Theorem, with an algorithm. 3 4These scripts contain theories to support the formalisation of an algorithm for Fermat's Two Squares Theorem. 5 6## Theory 7* __helper__, helper theorems for arithmetic, sets, maps and lists. 8* __involute__, basic properties of involution. 9* __involuteFix__, pairs and fixes of involution. 10* __involuteAction__, involution and group action. 11* __iterate__, iteration of a function, with period of iteration. 12* __iterateCompose__, iteration of involution composition. 13* __iterateCompute__, iteration period computation, recursion and while-loop. 14 15## Application 16* __windmill__, definitions of windmill, mill, flip, and zaiger. 17* __twoSquares__, existence, uniqueness and algorithm of two squares theorem. 18