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