- transcript: bugfix

[helm.git] / helm / software / matita / library / nat / chebyshev.ma

diff --git a/helm/software/matita/library/nat/chebyshev.ma b/helm/software/matita/library/nat/chebyshev.ma
index 6ef8624e4983922e9d8276633f72a6d0163d42fc..701ad7ad16ac82b14a05a6c27ed14524d9b98552 100644 (file)
--- 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