...

[helm.git] / helm / software / matita / dama / sequence.ma

diff --git a/helm/software/matita/dama/sequence.ma b/helm/software/matita/dama/sequence.ma
index 9edc871e5ce25ba2f2373d07b01aa6c82f74d043..1350545ae23863b86a04019befa86e293b1cd376 100644 (file)
--- a/helm/software/matita/dama/sequence.ma
+++ b/helm/software/matita/dama/sequence.ma
@@ -58,7 +58,12 @@ intros (O s x Ssup); elim Ssup (Ubx M); clear Ssup; split; [assumption]
 intros 3 (y Uby E); cases (M ? E) (n En); unfold in Uby; cases (Uby ? En);
 qed.
 
+include "ordered_group.ma".
+include "nat/orders.ma".
 
+definition tends ≝ 
+  λO:ogroup.λs:sequence O.
+    ∀e:O.0 < e → ∃N.∀n.N < n → -e < s n ∧ s n < e.
 
 definition increasing ≝ 
   λO:pordered_set.λa:sequence O.∀n:nat.a n ≤ a (S n).