Minor changes to make the script more robust to strategy changes.

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

diff --git a/matita/matita/lib/arithmetics/chebyshev/bertrand.ma b/matita/matita/lib/arithmetics/chebyshev/bertrand.ma
index 99770436b441a352f1504f2dbb25a81ef05d75d8..8f41262e3b7519b5bb843605504e5a31c0ebc4e4 100644 (file)
--- a/matita/matita/lib/arithmetics/chebyshev/bertrand.ma
+++ b/matita/matita/lib/arithmetics/chebyshev/bertrand.ma
@@ -166,7 +166,7 @@ elim (log p (2*n))
           [@leb_true_to_le //
           |>commutative_times in ⊢ (??%); > times_exp
            @(transitive_le ? (exp n 2))
-            [<associative_times >exp_2 in ⊢ (??%); @le_times //
+            [<associative_times >exp_2 in ⊢ (??%); @le_times [@le18|//]
             |@(le_exp1 … (lt_O_S ?))
              @(le_plus_to_le 3)
              cut (3+2*n/3*3 = S(2*n/3)*3) [//] #eq1 >eq1