3.11 !!!

[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 1350545ae23863b86a04019befa86e293b1cd376..52baef839d2856de7943f6c8a206ed3c6f97d0ad 100644 (file)
--- a/helm/software/matita/dama/sequence.ma
+++ b/helm/software/matita/dama/sequence.ma
@@ -72,6 +72,8 @@ definition decreasing ≝
   λO:pordered_set.λa:sequence O.∀n:nat.a (S n) ≤ a n.
 
 
+
+
 (*
 
 definition is_upper_bound ≝ λO:pordered_set.λa:sequence O.λu:O.∀n:nat.a n ≤ u.