This line, and those below, will be ignored--

[helm.git] / matita / matita / lib / arithmetics / chebyshev / chebyshev_psi.ma

diff --git a/matita/matita/lib/arithmetics/chebyshev/chebyshev_psi.ma b/matita/matita/lib/arithmetics/chebyshev/chebyshev_psi.ma
index 5c4e93bbacd14e86e8124282a47d04ba4b7748e8..26409e9ce2237a58b5c07c908dddec9a8cf53c13 100644 (file)
--- 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
   ]