header {* Comprehensive number theory *} theory Number_Theory imports Fib Residues Eratosthenes begin end