...

[helm.git] / matita / dama / reals.ma

diff --git a/matita/dama/reals.ma b/matita/dama/reals.ma
index c03fdf26bf6c4d6ef3a6eefecb57f5bdc4f41116..d57e6cfba62f8cada56b0da615a5b07fa5df3d12 100644 (file)
--- a/matita/dama/reals.ma
+++ b/matita/dama/reals.ma
@@ -39,7 +39,7 @@ definition max_seq: ∀R:real.∀x,y:R. nat → R.
   [ 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;