X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fvector_spaces.ma;h=6aaebd12bde8b9007229f21b9755b160d63df765;hb=b348a1a39e17b541fca17d2218a3b91bd7f1fece;hp=3165be2e68438aab66b00170c361b79a167485ce;hpb=c6b621c1df5abd9a8a1567991379768c435607dd;p=helm.git

diff --git a/helm/software/matita/dama/vector_spaces.ma b/helm/software/matita/dama/vector_spaces.ma
index 3165be2e6..6aaebd12b 100644
--- a/helm/software/matita/dama/vector_spaces.ma
+++ b/helm/software/matita/dama/vector_spaces.ma
@@ -123,11 +123,11 @@ definition tends_to :
  ∀R:real.∀V:vector_space R.∀d:distance ? V.∀f:nat→V.∀l:V.Prop.
 apply
   (λR:real.λV:vector_space R.λd:distance ? V.λf:nat→V.λl:V.
-    ∀n:nat.∃m:nat.∀j:nat. le m j →
+    ∀n:nat.∃m:nat.∀j:nat. m ≤ j →
      d (f j) l ≤ inv R (sum_field ? (S n)) ?);
  apply not_eq_sum_field_zero;
  unfold;
- auto new.
+ autobatch.
 qed.
 
 definition is_cauchy_seq : ∀R:real.\forall V:vector_space R.
@@ -136,12 +136,12 @@ definition is_cauchy_seq : ∀R:real.\forall V:vector_space R.
   (λR:real.λV: vector_space R. \lambda d:distance ? V.
    \lambda f:nat→V.
     ∀m:nat.
-     ∃n:nat.∀N. le n N →
+     ∃n:nat.∀N. n ≤ N →
       -(inv R (sum_field ? (S m)) ?) ≤ d (f N)  (f n)  ∧
       d (f N)  (f n)≤ inv R (sum_field R (S m)) ?);
  apply not_eq_sum_field_zero;
  unfold;
- auto.
+ autobatch.
 qed.
 
 definition is_complete ≝