+nat/chebyshev.ma nat/factorial2.ma nat/factorization.ma nat/log.ma nat/o.ma nat/pi_p.ma
+nat/log.ma datatypes/constructors.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/minimization.ma nat/primes.ma nat/relevant_equations.ma
+nat/chebyshev_thm.ma nat/neper.ma
+nat/div_and_mod_diseq.ma nat/lt_arith.ma
+nat/binomial.ma nat/factorial2.ma nat/iteration2.ma
+nat/neper.ma nat/binomial.ma nat/chebyshev.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/log.ma
+nat/sqrt.ma nat/compare.ma nat/log.ma nat/times.ma
+nat/chebyshev_teta.ma nat/binomial.ma nat/pi_p.ma