X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Farithmetics%2Fchebyshev%2Fchebyshev_psi.ma;h=26409e9ce2237a58b5c07c908dddec9a8cf53c13;hb=b4f76b0d8fa0e5365fb48e91474febe200b647a7;hp=5c4e93bbacd14e86e8124282a47d04ba4b7748e8;hpb=86a8649e0ce63e0860f0feac9833a72c876e5a18;p=helm.git

diff --git a/matita/matita/lib/arithmetics/chebyshev/chebyshev_psi.ma b/matita/matita/lib/arithmetics/chebyshev/chebyshev_psi.ma
index 5c4e93bba..26409e9ce 100644
--- a/matita/matita/lib/arithmetics/chebyshev/chebyshev_psi.ma
+++ b/matita/matita/lib/arithmetics/chebyshev/chebyshev_psi.ma
@@ -122,6 +122,7 @@ theorem lePsi_r2: ∀n.
        @monotonic_le_plus_r @lt_O_log //
        @le_S_S_to_le //
       ]
+
     ]
   |<Hn @le_n
   ]