# Fermat's Two Squares Theorem, with an algorithm.

These scripts contain theories to support the formalisation of an algorithm for Fermat's Two Squares Theorem.

## Theory
* __helper__, helper theorems for arithmetic, sets, maps and lists.
* __involute__, basic properties of involution.
* __involuteFix__, pairs and fixes of involution.
* __involuteAction__, involution and group action.
* __iterate__, iteration of a function, with period of iteration.
* __iterateCompose__, iteration of involution composition.
* __iterateCompute__, iteration period computation, recursion and while-loop.

## Application
* __windmill__, definitions of windmill, mill, flip, and zaiger.
* __twoSquares__, existence, uniqueness and algorithm of two squares theorem.