le x y ==> x \leq y (now possible because of a bug fix in coercion

serialization in .moo files)

diff --git a/matita/dama/ordered_fields_ch0.ma b/matita/dama/ordered_fields_ch0.ma
index 07f32fadef0d8eef0c5e3bb00101a197a5bb3910..1c3b0fe7c14fb00ebf72563fe4b4b6f2fdffaab2 100644 (file)
--- a/matita/dama/ordered_fields_ch0.ma
+++ b/matita/dama/ordered_fields_ch0.ma
@@ -121,7 +121,7 @@ axiom lt_zero_to_le_inv_zero:
 definition tends_to : ∀F:ordered_field_ch0.∀f:nat→F.∀l:F.Prop.
  apply
   (λF:ordered_field_ch0.λf:nat → F.λl:F.
-    ∀n:nat.∃m:nat.∀j:nat. le m j →
+    ∀n:nat.∃m:nat.∀j:nat.m ≤ j →
      l - (inv F (sum_field ? (S n)) ?) ≤ f j ∧
      f j ≤ l + (inv F (sum_field ? (S n)) ?));
  apply not_eq_sum_field_zero;
@@ -143,7 +143,7 @@ definition is_cauchy_seq : ∀F:ordered_field_ch0.∀f:nat→F.Prop.
  apply
   (λF:ordered_field_ch0.λf:nat→F.
     ∀m:nat.
-     ∃n:nat.∀N. le n N →
+     ∃n:nat.∀N.n ≤ N →
       -(inv ? (sum_field F (S m)) ?) ≤ f N - f n ∧
       f N - f n ≤ inv ? (sum_field F (S m)) ?);
  apply not_eq_sum_field_zero;

diff --git a/matita/dama/vector_spaces.ma b/matita/dama/vector_spaces.ma
index 3165be2e68438aab66b00170c361b79a167485ce..de4af986a7a98d437ecf2ed3e6d46892a1304396 100644 (file)
--- a/matita/dama/vector_spaces.ma
+++ b/matita/dama/vector_spaces.ma
@@ -123,7 +123,7 @@ 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;
@@ -136,7 +136,7 @@ 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;