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