refactoring

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

diff --git a/matita/matita/lib/arithmetics/chebyshev/bertrand256.ma b/matita/matita/lib/arithmetics/chebyshev/bertrand256.ma
index 163125b818ee1c7e10da82a53db299cc926e90a6..c65e6238112af4c666e0771a110ccd87bd87ba58 100644 (file)
--- 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.