X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Freals.ma;h=d57e6cfba62f8cada56b0da615a5b07fa5df3d12;hb=41a2cd9f8efb97c0e89c65adbd46d0ff751d2e6c;hp=9e458e29102df18e4d84b35767c7095fd110f85e;hpb=c6b621c1df5abd9a8a1567991379768c435607dd;p=helm.git

diff --git a/helm/software/matita/dama/reals.ma b/helm/software/matita/dama/reals.ma
index 9e458e291..d57e6cfba 100644
--- a/helm/software/matita/dama/reals.ma
+++ b/helm/software/matita/dama/reals.ma
@@ -35,11 +35,11 @@ qed.
 
 definition max_seq: ∀R:real.∀x,y:R. nat → R.
  intros (R x y);
- elim (of_cotransitive R 0 (inv ? (sum_field ? (S n)) ?) (x-y));
+ elim (cos_cotransitive R 0 (inv ? (sum_field ? (S n)) ?) (x-y));
   [ apply x
   | apply not_eq_sum_field_zero ;
     unfold;
-    auto new
+    autobatch
   | apply y
   | apply lt_zero_to_le_inv_zero 
   ].
@@ -147,7 +147,7 @@ lemma technical1: ∀R:real.lim R (to_zero R) (is_cauchy_seq_to_zero R) = 0.
  elim daemon.
 qed.
  
-lemma abs_x_ge_O: \forall R: real. \forall x:R. (zero R) ≤ abs R x.
+lemma abs_x_ge_O: ∀R:real.∀x:R. 0 ≤ abs ? x.
  intros;
  unfold abs;
  unfold max;
@@ -157,7 +157,7 @@ lemma abs_x_ge_O: \forall R: real. \forall x:R. (zero R) ≤ abs R x.
  unfold to_zero;
  unfold max_seq;
  elim
-     (of_cotransitive R 0
+     (cos_cotransitive R 0
 (inv R (sum_field R (S n))
  (not_eq_sum_field_zero R (S n) (le_S_S O n (le_O_n n)))) (x--x)
 (lt_zero_to_le_inv_zero R (S n)