X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Fchebyshev.ma;h=f7ffbf0460eb08cce593f98083167abe7f39b1dc;hb=c52605b5b949f2ceafbe788c8f7bf7e74dc89b5c;hp=c06675d0e2d3db98e1019496b3ed94887609fba5;hpb=2a4ee6db10333354003f6e3cd342298a82799ad4;p=helm.git

diff --git a/matita/library/nat/chebyshev.ma b/matita/library/nat/chebyshev.ma
index c06675d0e..f7ffbf046 100644
--- a/matita/library/nat/chebyshev.ma
+++ b/matita/library/nat/chebyshev.ma
@@ -1199,6 +1199,8 @@ apply (trans_le ? (B((S(S O))*n)*A n))
   ]
 qed.
 
+(*
+
 (* da spostare *)
 theorem times_exp: \forall n,m,p.exp n p * exp m p = exp (n*m) p.
 intros.elim p
@@ -1707,4 +1709,4 @@ elim (lt_O_to_or_eq_S m)
        
        a*log a-a+k*log a
        
-*)
\ No newline at end of file
+*)