section ‹Comprehensive number theory› theory Number_Theory imports Fib Residues Eratosthenes Mod_Exp Quadratic_Reciprocity Pocklington Prime_Powers Residue_Primitive_Roots begin end