+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.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;
+ unfold;
+ auto new.
+qed.
+
+(*
+definition is_cauchy_seq ≝
+ λF:ordered_field_ch0.λf:nat→F.
+ ∀eps:F. 0 < eps →
+ ∃n:nat.∀M. n ≤ M →
+ -eps ≤ f M - f n ∧ f M - f n ≤ eps.
+*)
+
+
+
+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.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;
+ unfold;
+ auto.
+qed.