X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fchebyshev.ma;h=701ad7ad16ac82b14a05a6c27ed14524d9b98552;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=6ef8624e4983922e9d8276633f72a6d0163d42fc;hpb=291771338278ef9c5b32e2f1660822b9246d7d0e;p=helm.git

diff --git a/helm/software/matita/library/nat/chebyshev.ma b/helm/software/matita/library/nat/chebyshev.ma
index 6ef8624e4..701ad7ad1 100644
--- a/helm/software/matita/library/nat/chebyshev.ma
+++ b/helm/software/matita/library/nat/chebyshev.ma
@@ -16,6 +16,7 @@ include "nat/log.ma".
 include "nat/pi_p.ma".
 include "nat/factorization.ma".
 include "nat/factorial2.ma".
+include "nat/o.ma".
 
 definition prim: nat \to nat \def
 \lambda n. sigma_p (S n) primeb (\lambda p.1).
@@ -2098,7 +2099,6 @@ apply (trans_le ? ((exp 2 (2*n))/(2*n)))
      rewrite < plus_n_O.
      rewrite > exp_plus_times.
      apply le_times_l.
-     alias id "le_times_SSO_n_exp_SSO_n" = "cic:/matita/nat/o/le_times_SSO_n_exp_SSO_n.con".
      apply le_times_SSO_n_exp_SSO_n
     ]
   |apply le_times_to_le_div2