X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Freals.ma;h=87bbee5fd0d2e84de0a9e49d8ee066f4d826e8b8;hb=38d3574438b4f764ad433915c9733cc73a684b39;hp=c03fdf26bf6c4d6ef3a6eefecb57f5bdc4f41116;hpb=603bbe202f09745133cefa4902f2b16fb17b70b8;p=helm.git

diff --git a/helm/software/matita/dama/reals.ma b/helm/software/matita/dama/reals.ma
index c03fdf26b..87bbee5fd 100644
--- a/helm/software/matita/dama/reals.ma
+++ b/helm/software/matita/dama/reals.ma
@@ -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;