X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fchebyshev%2Fbertrand256.ma;h=c65e6238112af4c666e0771a110ccd87bd87ba58;hb=774c5e125eb44693a5a760226713067c41baf09f;hp=163125b818ee1c7e10da82a53db299cc926e90a6;hpb=342278d86d2ebb11b046dcc9f44cc5d08cd16352;p=helm.git

diff --git a/matita/matita/lib/arithmetics/chebyshev/bertrand256.ma b/matita/matita/lib/arithmetics/chebyshev/bertrand256.ma
index 163125b81..c65e62381 100644
--- a/matita/matita/lib/arithmetics/chebyshev/bertrand256.ma
+++ b/matita/matita/lib/arithmetics/chebyshev/bertrand256.ma
@@ -236,6 +236,6 @@ theorem bertrand :
 ∀n. O < n → bertrand n.
 #n #posn elim (decidable_le n 256)
   [@bertrand_down //
-  |#len @le_to_bertrand2 @lt_to_le @not_le_to_lt @len]
+  |#len @bertrand_up @lt_to_le @not_le_to_lt @len]
 qed.