From 9483f7e6c85ec11f88bdb219b2cebad2039b1a74 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 23 Jan 2008 12:44:39 +0000
Subject: [PATCH] snapshot with more duality, almost where we left without
 duality

---
 helm/software/matita/dama/depends             |  12 +-
 helm/software/matita/dama/excess.ma           |  12 +-
 helm/software/matita/dama/infsup.ma           | 206 +++--------------
 helm/software/matita/dama/lattice.ma          |  90 +++++---
 helm/software/matita/dama/limit.ma            |  56 +++++
 helm/software/matita/dama/metric_lattice.ma   |  54 +----
 helm/software/matita/dama/metric_space.ma     |  25 +-
 helm/software/matita/dama/ordered_group.ma    |  10 +-
 helm/software/matita/dama/sandwich.ma         |  16 +-
 .../matita/dama/sandwich_corollary.ma         |   8 +-
 helm/software/matita/dama/sequence.ma         | 216 +-----------------
 helm/software/matita/dama/tend.ma             |  28 +++
 12 files changed, 211 insertions(+), 522 deletions(-)
 create mode 100644 helm/software/matita/dama/limit.ma
 create mode 100644 helm/software/matita/dama/tend.ma

diff --git a/helm/software/matita/dama/depends b/helm/software/matita/dama/depends
index e96472aa9..8334fa1a3 100644
--- a/helm/software/matita/dama/depends
+++ b/helm/software/matita/dama/depends
@@ -1,21 +1,23 @@
-metric_lattice.ma excess.ma lattice.ma metric_space.ma
+metric_lattice.ma lattice.ma metric_space.ma
 metric_space.ma ordered_divisible_group.ma
-sandwich.ma metric_lattice.ma nat/orders.ma nat/plus.ma sequence.ma
+sandwich.ma nat/orders.ma nat/plus.ma tend.ma
 premetric_lattice.ma lattice.ma metric_space.ma
 ordered_group.ma group.ma
 divisible_group.ma group.ma nat/orders.ma
 ordered_divisible_group.ma divisible_group.ma nat/orders.ma nat/times.ma ordered_group.ma
-sequence.ma excess.ma nat/orders.ma ordered_group.ma
+sequence.ma excess.ma
 constructive_connectives.ma logic/connectives.ma
 lattice.TF.ma excess.ma lattice.ma nat/nat.ma
 group.ma excess.ma
 prevalued_lattice.ma ordered_group.ma
 excess.ma constructive_connectives.ma constructive_higher_order_relations.ma higher_order_defs/relations.ma nat/plus.ma
-sandwich_corollary.ma metric_lattice.ma sandwich.ma
+sandwich_corollary.ma sandwich.ma
 Q_is_orded_divisble_group.ma Q/q.ma ordered_divisible_group.ma
+limit.ma excess.ma infsup.ma tend.ma
 lattice.ma excess.ma
+tend.ma metric_lattice.ma nat/orders.ma sequence.ma
 constructive_higher_order_relations.ma constructive_connectives.ma higher_order_defs/relations.ma
-infsup.ma sandwich_corollary.ma
+infsup.ma excess.ma sequence.ma
 constructive_pointfree/lebesgue.ma constructive_connectives.ma metric_lattice.ma sequence.ma
 classical_pointwise/topology.ma classical_pointwise/sets.ma
 classical_pointwise/sigma_algebra.ma classical_pointwise/topology.ma
diff --git a/helm/software/matita/dama/excess.ma b/helm/software/matita/dama/excess.ma
index 959e866fd..826ae8c0b 100644
--- a/helm/software/matita/dama/excess.ma
+++ b/helm/software/matita/dama/excess.ma
@@ -51,18 +51,18 @@ qed.
 
 record excess_ : Type ≝ {
   exc_exc:> excess_base;
-  exc_ap: apartness;
-  exc_with: ap_carr exc_ap = exc_carr exc_exc
+  exc_ap_: apartness;
+  exc_with: ap_carr exc_ap_ = exc_carr exc_exc
 }.
 
-definition apart_of_excess_: excess_ → apartness.
+definition exc_ap: excess_ → apartness.
 intro E; apply (mk_apartness E); unfold Type_OF_excess_; 
 cases (exc_with E); simplify;
-[apply (ap_apart (exc_ap E));
+[apply (ap_apart (exc_ap_ E));
 |apply ap_coreflexive;|apply ap_symmetric;|apply ap_cotransitive] 
 qed.
 
-coercion cic:/matita/excess/apart_of_excess_.con.
+coercion cic:/matita/excess/exc_ap.con.
 
 record excess : Type ≝ {
   excess_carr:> excess_;
@@ -245,7 +245,7 @@ intro E; apply mk_excess;
       [ apply (λx,y:E.y≰x);|apply exc_coreflexive;
       | unfold cotransitive; simplify; intros (x y z H);
         cases (exc_cotransitive E ??z H);[right|left]assumption]
-  |2: apply (exc_ap E);
+  |2: apply (exc_ap_ E);
   |3: apply (exc_with E);]
 |2: simplify; intros (y x H); fold simplify (y#x) in H;
     apply ap2exc; apply ap_symmetric; apply H;
diff --git a/helm/software/matita/dama/infsup.ma b/helm/software/matita/dama/infsup.ma
index b3babd1b5..60c4d2f81 100644
--- a/helm/software/matita/dama/infsup.ma
+++ b/helm/software/matita/dama/infsup.ma
@@ -12,190 +12,38 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "sandwich_corollary.ma".
+include "sequence.ma".
 
-(* 3.19 *)
-definition supremum ≝ 
-  λR.λml:mlattice R.λxn:sequence ml.λx:ml.
-    increasing ? xn → upper_bound ? xn x ∧ xn ⇝ x.
+definition upper_bound ≝ λO:excess.λa:sequence O.λu:O.∀n:nat.a n ≤ u.
 
-definition infimum ≝ 
-  λR.λml:mlattice R.λxn:sequence ml.λx:ml.
-    decreasing ? xn → lower_bound ? xn x ∧ xn ⇝ x.
-    
-(* 3.20 *)
-lemma supremum_uniq:
-  ∀R.∀ml:mlattice R.∀xn:sequence ml.increasing ? xn → 
-   ∀x,y:ml.supremum ?? xn x → supremum ?? xn y → δ x y ≈ 0.
-intros (R ml xn Hxn x y Sx Sy);
-elim (Sx Hxn) (_ Hx); elim (Sy Hxn) (_ Hy);
-apply (tends_uniq ?? xn ?? Hx Hy);
-qed.
+definition strong_sup ≝
+  λO:excess.λs:sequence O.λx.upper_bound ? s x ∧ (∀y:O.x ≰ y → ∃n.s n ≰ y).
 
-definition shift : ∀R.∀ml:mlattice R.∀xn:sequence ml.nat → sequence ml ≝
- λR.λml:mlattice R.λxn:sequence ml.λm:nat.λn.xn (n+m).
- 
-definition ank ≝
-  λR.λml:mlattice R.λxn:sequence ml.λk:nat.
-    let rec ank_aux (i : nat) ≝
-      match i with 
-      [ O ⇒ (shift ?? xn k) O
-      | S n1 ⇒ (shift ?? xn k) (S n1) ∧ ank_aux n1]
-    in ank_aux.
-     
-notation < "'a'\sup k" non associative with precedence 50 for
- @{ 'ank $x $k }.
- 
-interpretation "ank" 'ank x k =
- (cic:/matita/infsup/ank.con _ _ x k).      
+definition increasing ≝ λO:excess.λa:sequence O.∀n:nat.a n ≤ a (S n).
 
-notation < "'a'(k \atop n)" non associative with precedence 50 for
- @{ 'ank2 $x $k $n }.
- 
-interpretation "ank2" 'ank2 x k n =
- (cic:/matita/infsup/ank.con _ _ x k n).      
-    
-definition bnk ≝
-  λR.λml:mlattice R.λxn:sequence ml.λk:nat.
-    let rec bnk_aux (i : nat) ≝
-      match i with 
-      [ O ⇒ (shift ?? xn k) O
-      | S n1 ⇒ (shift ?? xn k) (S n1) ∨ bnk_aux n1]
-    in bnk_aux.
+notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 50 for @{'upper_bound $s $x}.
+notation < "x \nbsp 'is_lower_bound' \nbsp s" non associative with precedence 50 for @{'lower_bound $s $x}.
+notation < "s \nbsp 'is_increasing'"          non associative with precedence 50 for @{'increasing $s}.
+notation < "s \nbsp 'is_decreasing'"          non associative with precedence 50 for @{'decreasing $s}.
+notation < "x \nbsp 'is_strong_sup' \nbsp s"  non associative with precedence 50 for @{'strong_sup $s $x}.
+notation < "x \nbsp 'is_strong_inf' \nbsp s"  non associative with precedence 50 for @{'strong_inf $s $x}.
 
-notation < "'b'\sup k" non associative with precedence 50 for
- @{ 'bnk $x $k }.
- 
-interpretation "bnk" 'bnk x k =
- (cic:/matita/infsup/bnk.con _ _ x k).      
+notation > "x 'is_upper_bound' s" non associative with precedence 50 for @{'upper_bound $s $x}.
+notation > "x 'is_lower_bound' s" non associative with precedence 50 for @{'lower_bound $s $x}.
+notation > "s 'is_increasing'"    non associative with precedence 50 for @{'increasing $s}.
+notation > "s 'is_decreasing'"    non associative with precedence 50 for @{'decreasing $s}.
+notation > "x 'is_strong_sup' s"  non associative with precedence 50 for @{'strong_sup $s $x}.
+notation > "x 'is_strong_inf' s"  non associative with precedence 50 for @{'strong_inf $s $x}.
 
-notation < "('b' \sup k) \sub n" non associative with precedence 50 for
- @{ 'bnk2 $x $k $n }.
- 
-interpretation "bnk2" 'bnk2 x k n =
- (cic:/matita/infsup/bnk.con _ _ x k n).      
-    
-lemma ank_decreasing: 
-  ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k.decreasing ? (ank ?? xn k).
-intros (R ml xn k); unfold; intro n; simplify; apply lem;
-qed.
+interpretation "Excess upper bound" 'upper_bound s x = (cic:/matita/infsup/upper_bound.con _ s x).
+interpretation "Excess lower bound" 'lower_bound s x = (cic:/matita/infsup/upper_bound.con (cic:/matita/excess/dual_exc.con _) s x).
+interpretation "Excess increasing"  'increasing s    = (cic:/matita/infsup/increasing.con _ s).
+interpretation "Excess decreasing"  'decreasing s    = (cic:/matita/infsup/increasing.con (cic:/matita/excess/dual_exc.con _) s).
+interpretation "Excess strong sup"  'strong_sup s x  = (cic:/matita/infsup/strong_sup.con _ s x).
+interpretation "Excess strong inf"  'strong_inf s x  = (cic:/matita/infsup/strong_sup.con (cic:/matita/excess/dual_exc.con _) s x).
 
-(* 3.26 *)
-lemma ankS:
-  ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n:nat.
-   ((ank ?? xn k) (S n)) ≈ (xn k ∧ ank ?? xn (S k) n).
-intros (R ml xn k n); elim n; simplify; [apply meet_comm]  
-simplify in H; apply (Eq≈ ? (feq_ml ???? (H))); clear H;
-apply (Eq≈ ? (meet_assoc ????));    
-apply (Eq≈ ?? (eq_sym ??? (meet_assoc ????)));
-apply feq_mr; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
-simplify; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
-apply meet_comm;
-qed.    
+definition seq_dual_exc_hint: ∀E.sequence E → sequence (dual_exc E) ≝ λE.λx:sequence E.x.
+definition seq_dual_exc_hint1: ∀E.sequence (dual_exc E) → sequence E ≝ λE.λx:sequence (dual_exc E).x.
 
-lemma bnkS:
-  ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n:nat.
-   ((bnk ?? xn k) (S n)) ≈ (xn k ∨ bnk ?? xn (S k) n).
-intros (R ml xn k n); elim n; simplify; [apply join_comm]  
-simplify in H; apply (Eq≈ ? (feq_jl ???? (H))); clear H;
-apply (Eq≈ ? (join_assoc ????));    
-apply (Eq≈ ?? (eq_sym ??? (join_assoc ????)));
-apply feq_jr; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
-simplify; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
-apply join_comm;
-qed.    
-
-lemma le_asnk_ansk:
-  ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n.
-   (ank ?? xn k (S n)) ≤ (ank ?? xn (S k) n).
-intros (R ml xn k n);
-apply (Le≪ (xn k ∧ ank ?? xn (S k) n) (ankS ?????)); apply lem;
-qed.   
-
-lemma le_bnsk_bsnk:
-  ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n.
-   (bnk ?? xn (S k) n) ≤ (bnk ?? xn k (S n)).
-intros (R ml xn k n);
-apply (Le≫ (xn k ∨ bnk ?? xn (S k) n) (bnkS ?????)); 
-apply (Le≫ ? (join_comm ???));
-apply lej;
-qed.   
-
-
-(* 3.27 *)
-lemma inf_increasing:
-  ∀R.∀ml:mlattice R.∀xn:sequence ml.
-   ∀alpha:sequence ml. (∀k.strong_inf ml (ank ?? xn k) (alpha k)) → 
-     increasing ml alpha.
-intros (R ml xn alpha H); unfold strong_inf in H; unfold lower_bound in H; unfold; 
-intro r; 
-elim (H r) (H1r H2r);
-elim (H (S r)) (H1sr H2sr); clear H H2r H1sr;
-intro e; cases (H2sr ? e) (w Hw); clear e H2sr;
-lapply (H1r (S w)) as Hsw; clear H1r;
-lapply (le_transitive ???? Hsw (le_asnk_ansk ?????)) as H;
-cases (H Hw);
-qed.
-
-lemma sup_decreasing:
-  ∀R.∀ml:mlattice R.∀xn:sequence ml.
-   ∀alpha:sequence ml. (∀k.strong_sup ml (bnk ?? xn k) (alpha k)) → 
-     decreasing ml alpha.
-intros (R ml xn alpha H); unfold strong_sup in H; unfold upper_bound in H; unfold; 
-intro r; 
-elim (H r) (H1r H2r);
-elim (H (S r)) (H1sr H2sr); clear H H2r H1sr;
-intro e; cases (H2sr ? e) (w Hw); clear e H2sr;
-lapply (H1r (S w)) as Hsw; clear H1r;
-lapply (le_transitive ???? (le_bnsk_bsnk ?????) Hsw) as H;
-cases (H Hw);
-qed.
-
-(* 3.28 *)
-definition liminf ≝
-  λR.λml:mlattice R.λxn:sequence ml.λx:ml.   
-    ∃alpha:sequence ml. 
-      (∀k.strong_inf ml (ank ?? xn k) (alpha k)) ∧ strong_sup ml alpha x.
-  
-definition limsup ≝
-  λR.λml:mlattice R.λxn:sequence ml.λx:ml.   
-    ∃alpha:sequence ml. 
-      (∀k.strong_sup ml (bnk ?? xn k) (alpha k)) ∧ strong_inf ml alpha x.
-  
-(* 3.29 *)  
-alias symbol "and" = "constructive and".
-definition lim ≝
-  λR.λml:mlattice R.λxn:sequence ml.λx:ml.   
-   (*∃y,z.*)limsup ?? xn x ∧ liminf ?? xn x(* ∧ y ≈ x ∧ z ≈ x*).
-  
-(* 3.30 *)   
-lemma lim_uniq: ∀R.∀ml:mlattice R.∀xn:sequence ml.∀x:ml.
-   lim ?? xn x → xn ⇝ x.
-intros (R ml xn x Hl); 
-unfold in Hl; unfold limsup in Hl; unfold liminf in Hl; 
-(* decompose; *)
-elim Hl (low Hl_); clear Hl;   
-elim Hl_ (up Hl); clear Hl_;  
-elim Hl (Hl_ E1); clear Hl;   
-elim Hl_ (Hl E2); clear Hl_;  
-elim Hl (H1 H2); clear Hl;   
-elim H1 (alpha Halpha); clear H1;   
-elim H2 (beta Hbeta); clear H2;
-apply (sandwich ?? alpha beta); 
-[1: intro m; elim Halpha (Ha5 Ha6); clear Halpha;
-    lapply (sup_increasing ????? Ha6) as Ha7;
-
-    unfold strong_sup in Halpha Hbeta;
-    unfold strong_inf in Halpha Hbeta;
-    unfold lower_bound in Halpha Hbeta;
-    unfold upper_bound in Halpha Hbeta; 
-    elim (Halpha m) (Ha5 Ha6); clear Halpha;
-    elim Ha5 (Ha1 Ha2); clear Ha5;
-    elim Ha6 (Ha3 Ha4); clear Ha6;
-    split; 
-    [1: intro H; elim (Ha2 ? H) (w H1);
-        elim (Ha4 ? H1);
-    
-    
-    
-  
\ No newline at end of file
+coercion cic:/matita/infsup/seq_dual_exc_hint.con nocomposites.
+coercion cic:/matita/infsup/seq_dual_exc_hint1.con nocomposites.
diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma
index 83d138526..ef0213425 100644
--- a/helm/software/matita/dama/lattice.ma
+++ b/helm/software/matita/dama/lattice.ma
@@ -71,26 +71,26 @@ qed.
 
 record semi_lattice : Type ≝ {
   sl_exc:> excess;
-  meet: sl_exc → sl_exc → sl_exc;
-  meet_refl: ∀x.meet x x ≈ x;  
-  meet_comm: ∀x,y. meet x y ≈ meet y x;
-  meet_assoc: ∀x,y,z. meet x (meet y z) ≈ meet (meet x y) z;
-  strong_extm: ∀x.strong_ext ? (meet x);
-  le_to_eqm: ∀x,y.x ≤ y → x ≈ meet x y;
-  lem: ∀x,y.(meet x y) ≤ y 
+  sl_meet: sl_exc → sl_exc → sl_exc;
+  sl_meet_refl: ∀x.sl_meet x x ≈ x;  
+  sl_meet_comm: ∀x,y. sl_meet x y ≈ sl_meet y x;
+  sl_meet_assoc: ∀x,y,z. sl_meet x (sl_meet y z) ≈ sl_meet (sl_meet x y) z;
+  sl_strong_extm: ∀x.strong_ext ? (sl_meet x);
+  sl_le_to_eqm: ∀x,y.x ≤ y → x ≈ sl_meet x y;
+  sl_lem: ∀x,y.(sl_meet x y) ≤ y 
 }.
  
-interpretation "semi lattice meet" 'and a b = (cic:/matita/lattice/meet.con _ a b).
+interpretation "semi lattice meet" 'and a b = (cic:/matita/lattice/sl_meet.con _ a b).
 
-lemma feq_ml: ∀ml:semi_lattice.∀a,b,c:ml. a ≈ b → (c ∧ a) ≈ (c ∧ b).
+lemma sl_feq_ml: ∀ml:semi_lattice.∀a,b,c:ml. a ≈ b → (c ∧ a) ≈ (c ∧ b).
 intros (l a b c H); unfold eq in H ⊢ %; unfold Not in H ⊢ %;
-intro H1; apply H; clear H; apply (strong_extm ???? H1);
+intro H1; apply H; clear H; apply (sl_strong_extm ???? H1);
 qed.
 
-lemma feq_mr: ∀ml:semi_lattice.∀a,b,c:ml. a ≈ b → (a ∧ c) ≈ (b ∧ c).
+lemma sl_feq_mr: ∀ml:semi_lattice.∀a,b,c:ml. a ≈ b → (a ∧ c) ≈ (b ∧ c).
 intros (l a b c H); 
-apply (Eq≈ ? (meet_comm ???)); apply (Eq≈ ?? (meet_comm ???));
-apply feq_ml; assumption;
+apply (Eq≈ ? (sl_meet_comm ???)); apply (Eq≈ ?? (sl_meet_comm ???));
+apply sl_feq_ml; assumption;
 qed.
  
  
@@ -173,17 +173,17 @@ intro l;
 apply (mk_semi_lattice (dual_exc l)); 
 unfold excess_OF_lattice_;
 cases (latt_with l); simplify;
-[apply meet|apply meet_refl|apply meet_comm|apply meet_assoc|
-apply strong_extm| apply le_to_eqm|apply lem]
+[apply sl_meet|apply sl_meet_refl|apply sl_meet_comm|apply sl_meet_assoc|
+apply sl_strong_extm| apply sl_le_to_eqm|apply sl_lem]
 qed. 
  
 coercion cic:/matita/lattice/latt_jcarr.con.
 
 interpretation "Lattice meet" 'and a b =
- (cic:/matita/lattice/meet.con (cic:/matita/lattice/latt_mcarr.con _) a b).  
+ (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_mcarr.con _) a b).  
 
 interpretation "Lattice join" 'or a b =
- (cic:/matita/lattice/meet.con (cic:/matita/lattice/latt_jcarr.con _) a b).  
+ (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_jcarr.con _) a b).  
 
 record lattice : Type ≝ {
   latt_carr:> lattice_;
@@ -206,27 +206,47 @@ notation "'strong_extj'" non associative with precedence 50 for @{'strong_extj}.
 notation "'le_to_eqj'"   non associative with precedence 50 for @{'le_to_eqj}.
 notation "'lej'"         non associative with precedence 50 for @{'lej}.
 
-interpretation "Lattice meet"        'meet = (cic:/matita/lattice/meet.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice meet_refl"   'meet_refl = (cic:/matita/lattice/meet_refl.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice meet_comm"   'meet_comm = (cic:/matita/lattice/meet_comm.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice meet_assoc"  'meet_assoc = (cic:/matita/lattice/meet_assoc.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice strong_extm" 'strong_extm = (cic:/matita/lattice/strong_extm.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice le_to_eqm"   'le_to_eqm = (cic:/matita/lattice/le_to_eqm.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice lem"         'lem = (cic:/matita/lattice/lem.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice join"        'join = (cic:/matita/lattice/meet.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice join_refl"   'join_refl = (cic:/matita/lattice/meet_refl.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice join_comm"   'join_comm = (cic:/matita/lattice/meet_comm.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice join_assoc"  'join_assoc = (cic:/matita/lattice/meet_assoc.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice strong_extm" 'strong_extj = (cic:/matita/lattice/strong_extm.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice le_to_eqj"   'le_to_eqj = (cic:/matita/lattice/le_to_eqm.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice lej"         'lej = (cic:/matita/lattice/lem.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice meet"        'meet        = (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice meet_refl"   'meet_refl   = (cic:/matita/lattice/sl_meet_refl.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice meet_comm"   'meet_comm   = (cic:/matita/lattice/sl_meet_comm.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice meet_assoc"  'meet_assoc  = (cic:/matita/lattice/sl_meet_assoc.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice strong_extm" 'strong_extm = (cic:/matita/lattice/sl_strong_extm.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice le_to_eqm"   'le_to_eqm   = (cic:/matita/lattice/sl_le_to_eqm.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice lem"         'lem         = (cic:/matita/lattice/sl_lem.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice join"        'join        = (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice join_refl"   'join_refl   = (cic:/matita/lattice/sl_meet_refl.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice join_comm"   'join_comm   = (cic:/matita/lattice/sl_meet_comm.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice join_assoc"  'join_assoc  = (cic:/matita/lattice/sl_meet_assoc.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice strong_extm" 'strong_extj = (cic:/matita/lattice/sl_strong_extm.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice le_to_eqj"   'le_to_eqj   = (cic:/matita/lattice/sl_le_to_eqm.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice lej"         'lej         = (cic:/matita/lattice/sl_lem.con (cic:/matita/lattice/latt_jcarr.con _)).
 
 notation "'feq_jl'" non associative with precedence 50 for @{'feq_jl}.
 notation "'feq_jr'" non associative with precedence 50 for @{'feq_jr}.
-interpretation "Lattice feq_jl" 'feq_jl = (cic:/matita/lattice/feq_ml.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice feq_jr" 'feq_jr = (cic:/matita/lattice/feq_mr.con (cic:/matita/lattice/latt_jcarr.con _)).
 notation "'feq_ml'" non associative with precedence 50 for @{'feq_ml}.
 notation "'feq_mr'" non associative with precedence 50 for @{'feq_mr}.
-interpretation "Lattice feq_ml" 'feq_ml = (cic:/matita/lattice/feq_ml.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice feq_mr" 'feq_mr = (cic:/matita/lattice/feq_mr.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice feq_jl" 'feq_jl = (cic:/matita/lattice/sl_feq_ml.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice feq_jr" 'feq_jr = (cic:/matita/lattice/sl_feq_mr.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice feq_ml" 'feq_ml = (cic:/matita/lattice/sl_feq_ml.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice feq_mr" 'feq_mr = (cic:/matita/lattice/sl_feq_mr.con (cic:/matita/lattice/latt_mcarr.con _)).
 
+
+interpretation "Lattive meet le" 'leq a b =
+ (cic:/matita/excess/le.con (cic:/matita/lattice/excess_OF_lattice1.con _) a b).
+
+interpretation "Lattive join le (aka ge)" 'geq a b =
+ (cic:/matita/excess/le.con (cic:/matita/lattice/excess_OF_lattice.con _) a b).
+
+(* these coercions help unification, handmaking a bit of conversion 
+   over an open term 
+*)
+lemma le_to_ge: ∀l:lattice.∀a,b:l.a ≤ b → b ≥ a.
+intros(l a b H); apply H;
+qed.
+
+lemma ge_to_le: ∀l:lattice.∀a,b:l.b ≥ a → a ≤ b.
+intros(l a b H); apply H;
+qed.
+
+coercion cic:/matita/lattice/le_to_ge.con nocomposites.
+coercion cic:/matita/lattice/ge_to_le.con nocomposites.
\ No newline at end of file
diff --git a/helm/software/matita/dama/limit.ma b/helm/software/matita/dama/limit.ma
new file mode 100644
index 000000000..14a0637b3
--- /dev/null
+++ b/helm/software/matita/dama/limit.ma
@@ -0,0 +1,56 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "infsup.ma".
+
+(* 3.28 *)
+definition limsup ≝
+  λE:excess.λxn:sequence E.λx:E.∃alpha:sequence E. 
+    (∀k.(alpha k) is_strong_sup xn) ∧ x is_strong_inf alpha.
+
+notation < "x \nbsp 'is_limsup' \nbsp s" non associative with precedence 50 for @{'limsup $s $x}.
+notation < "x \nbsp 'is_liminf' \nbsp s" non associative with precedence 50 for @{'liminf $s $x}.
+notation > "x 'is_limsup' s" non associative with precedence 50 for @{'limsup $s $x}.
+notation > "x 'is_liminf' s" non associative with precedence 50 for @{'liminf $s $x}.
+
+interpretation "Excess limsup" 'limsup s x = (cic:/matita/limit/limsup.con _ s x).
+interpretation "Excess liminf" 'liminf s x = (cic:/matita/limit/limsup.con (cic:/matita/excess/dual_exc.con _) s x).
+
+(* 3.29 *)  
+definition lim ≝ λE:excess.λxn:sequence E.λx:E. x is_limsup xn ∧ x is_liminf xn.
+
+notation < "x \nbsp 'is_lim' \nbsp s" non associative with precedence 50 for @{'lim $s $x}.
+notation > "x 'is_lim' s" non associative with precedence 50 for @{'lim $s $x}.
+interpretation "Excess lim" 'lim s x = (cic:/matita/limit/lim.con _ s x).
+
+lemma sup_decreasing:
+  ∀E:excess.∀xn:sequence E.
+   ∀alpha:sequence E. (∀k.(alpha k) is_strong_sup xn) → 
+     alpha is_decreasing.
+intros (E xn alpha H); unfold strong_sup in H; unfold upper_bound in H; unfold;
+intro r; 
+elim (H r) (H1r H2r);
+elim (H (S r)) (H1sr H2sr); clear H H2r H1sr;
+intro e; cases (H2sr (alpha r) e) (w Hw); clear e H2sr;
+cases (H1r w Hw);
+qed.
+
+include "tend.ma".
+  
+(* 3.30 *)   
+lemma lim_tends: 
+  ∀R.∀ml:mlattice R.∀xn:sequence ml.∀x:ml.
+    x is_lim xn → xn ⇝ x.
+intros (R ml xn x Hl); unfold lim in Hl; unfold limsup in Hl;
+
diff --git a/helm/software/matita/dama/metric_lattice.ma b/helm/software/matita/dama/metric_lattice.ma
index 968ae8f3b..9f5811b6d 100644
--- a/helm/software/matita/dama/metric_lattice.ma
+++ b/helm/software/matita/dama/metric_lattice.ma
@@ -18,25 +18,25 @@ include "lattice.ma".
 record mlattice_ (R : todgroup) : Type ≝ {
   ml_mspace_: metric_space R;
   ml_lattice:> lattice;
-  ml_with_: ms_carr ? ml_mspace_ = apart_of_excess (pl_carr ml_lattice) 
+  ml_with: ms_carr ? ml_mspace_ = Type_OF_lattice ml_lattice 
 }.
 
 lemma ml_mspace: ∀R.mlattice_ R → metric_space R.
-intros (R ml); apply (mk_metric_space R (apart_of_excess ml)); 
-unfold apartness_OF_mlattice_; 
-[rewrite < (ml_with_ ? ml); apply (metric ? (ml_mspace_ ? ml))]
-cases (ml_with_ ? ml); simplify;
-[apply (mpositive ? (ml_mspace_ ? ml));|apply (mreflexive ? (ml_mspace_ ? ml));
-|apply (msymmetric ? (ml_mspace_ ? ml));|apply (mtineq ? (ml_mspace_ ? ml))]
+intros  (R ml); apply (mk_metric_space R (Type_OF_mlattice_ ? ml));
+unfold Type_OF_mlattice_; cases (ml_with ? ml); simplify;
+[apply (metric ? (ml_mspace_ ? ml));|apply (mpositive ? (ml_mspace_ ? ml));
+|apply (mreflexive ? (ml_mspace_ ? ml));|apply (msymmetric ? (ml_mspace_ ? ml));
+|apply (mtineq ? (ml_mspace_ ? ml))]
 qed.
 
 coercion cic:/matita/metric_lattice/ml_mspace.con.
 
 alias symbol "plus" = "Abelian group plus".
+alias symbol "leq" = "ordered sets less or equal than".
 record mlattice (R : todgroup) : Type ≝ {
   ml_carr :> mlattice_ R;
   ml_prop1: ∀a,b:ml_carr. 0 < δ a b → a # b;
-  ml_prop2: ∀a,b,c:ml_carr. δ (a∨b) (a∨c) + δ (a∧b) (a∧c) ≤ δ b c
+  ml_prop2: ∀a,b,c:ml_carr. δ (a∨b) (a∨c) + δ (a∧b) (a∧c) ≤ (δ b c)
 }.
 
 lemma eq_to_ndlt0: ∀R.∀ml:mlattice R.∀a,b:ml. a ≈ b → ¬ 0 < δ a b.
@@ -65,7 +65,6 @@ lemma meq_r: ∀R.∀ml:mlattice R.∀x,y,z:ml. x≈z → δy x ≈ δy z.
 intros; apply (eq_trans ???? (msymmetric ??y x));
 apply (eq_trans ????? (msymmetric ??z y)); apply meq_l; assumption;
 qed.
- 
 
 lemma dap_to_lt: ∀R.∀ml:mlattice R.∀x,y:ml. δ x y # 0 → 0 < δ x y.
 intros; split [apply mpositive] apply ap_symmetric; assumption;
@@ -76,31 +75,6 @@ intros (R ml x y H); apply ml_prop1; split; [apply mpositive;]
 apply ap_symmetric; assumption;
 qed.
 
-interpretation "Lattive meet le" 'leq a b =
- (cic:/matita/excess/le.con (cic:/matita/lattice/excess_OF_lattice1.con _) a b).
-
-interpretation "Lattive join le (aka ge)" 'geq a b =
- (cic:/matita/excess/le.con (cic:/matita/lattice/excess_OF_lattice.con _) a b).
-
-lemma le_to_ge: ∀l:lattice.∀a,b:l.a ≤ b → b ≥ a.
-intros(l a b H); apply H;
-qed.
-
-lemma ge_to_le: ∀l:lattice.∀a,b:l.b ≥ a → a ≤ b.
-intros(l a b H); apply H;
-qed.
-
-lemma eq_to_eq:∀l:lattice.∀a,b:l.
-  (eq (apart_of_excess (pl_carr (latt_jcarr l))) a b) →
-  (eq (apart_of_excess (pl_carr (latt_mcarr l))) a b).
-intros 3; unfold eq; unfold apartness_OF_lattice;
-unfold apartness_OF_lattice_1; unfold latt_jcarr; simplify;
-unfold dual_exc; simplify; intros 2 (H H1); apply H;
-cases H1;[right|left]assumption;
-qed. 
-
-coercion cic:/matita/metric_lattice/eq_to_eq.con nocomposites.
-
 (* 3.11 *)
 lemma le_mtri: 
   ∀R.∀ml:mlattice R.∀x,y,z:ml. x ≤ y → y ≤ z → δ x z ≈ δ x y + δ y z.
@@ -109,22 +83,18 @@ apply (le_transitive ????? (ml_prop2 ?? (y) ??));
 cut ( δx y+ δy z ≈ δ(y∨x) (y∨z)+ δ(y∧x) (y∧z)); [
   apply (le_rewr ??? (δx y+ δy z)); [assumption] apply le_reflexive]
 lapply (le_to_eqm ?? Lxy) as Dxm; lapply (le_to_eqm ?? Lyz) as Dym;
-lapply (le_to_eqj ?? (le_to_ge ??? Lxy)) as Dxj; lapply (le_to_eqj ?? (le_to_ge ??? Lyz)) as Dyj; clear Lxy Lyz;
+lapply (le_to_eqj ?? Lxy) as Dxj; lapply (le_to_eqj ?? Lyz) as Dyj; clear Lxy Lyz;
 apply (Eq≈ (δ(x∧y) y + δy z) (meq_l ????? Dxm));
 apply (Eq≈ (δ(x∧y) (y∧z) + δy z) (meq_r ????? Dym));
 apply (Eq≈ (δ(x∧y) (y∧z) + δ(y∨x) z));[
-  apply feq_plusl; apply meq_l; clear Dyj Dxm Dym;
-  unfold apartness_OF_mlattice1;
-  exact (eq_to_eq ??? Dxj);]
+  apply feq_plusl; apply meq_l; clear Dyj Dxm Dym; assumption]
 apply (Eq≈ (δ(x∧y) (y∧z) + δ(y∨x) (z∨y))); [
   apply (feq_plusl ? (δ(x∧y) (y∧z)) ?? (meq_r ??? (y∨x) ? Dyj));]
 apply (Eq≈ ? (plus_comm ???));
 apply (Eq≈ (δ(y∨x) (y∨z)+ δ(x∧y) (y∧z)));[
-  apply feq_plusr;
-  apply meq_r; 
-  apply (join_comm y z);]
+  apply feq_plusr; apply meq_r; apply (join_comm ??);]
 apply feq_plusl;
-apply (Eq≈ (δ(y∧x) (y∧z)) (meq_l ????? (meet_comm x y)));
+apply (Eq≈ (δ(y∧x) (y∧z)) (meq_l ????? (meet_comm ??)));
 apply eq_reflexive;   
 qed.  
 
diff --git a/helm/software/matita/dama/metric_space.ma b/helm/software/matita/dama/metric_space.ma
index 2ea43c03a..2266fe9e9 100644
--- a/helm/software/matita/dama/metric_space.ma
+++ b/helm/software/matita/dama/metric_space.ma
@@ -12,11 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-
-
 include "ordered_divisible_group.ma".
 
-record metric_space (R : todgroup) : Type ≝ {
+record metric_space (R: todgroup) : Type ≝ {
   ms_carr :> Type;
   metric: ms_carr → ms_carr → R;
   mpositive: ∀a,b:ms_carr. 0 ≤ metric a b; 
@@ -30,24 +28,19 @@ interpretation "metric" 'delta2 a b = (cic:/matita/metric_space/metric.con _ _ a
 notation "\delta" non associative with precedence 80 for @{ 'delta }.
 interpretation "metric" 'delta = (cic:/matita/metric_space/metric.con _ _).
 
-definition apart_metric:=
-  λR.λms:metric_space R.λa,b:ms.0 < δ a b.
-
-lemma apart_of_metric_space: ∀R:todgroup.metric_space R → apartness.
-intros (R ms); apply (mk_apartness ? (apart_metric ? ms)); unfold apart_metric; unfold;
-[1: intros 2 (x H); cases H (H1 H2); 
-    lapply (ap_rewr ???? (eq_sym ??? (mreflexive ??x)) H2);
+lemma apart_of_metric_space: ∀R.metric_space R → apartness.
+intros (R ms); apply (mk_apartness ? (λa,b:ms.0 < δ a b)); unfold;
+[1: intros 2 (x H); cases H (H1 H2); clear H; 
+    lapply (Ap≫ ? (eq_sym ??? (mreflexive ??x)) H2);
     apply (ap_coreflexive R 0); assumption;
 |2: intros (x y H); cases H; split;
-    [1: apply (le_rewr ???? (msymmetric ????)); assumption
-    |2: apply (ap_rewr ???? (msymmetric ????)); assumption]
-|3: simplify; intros (x y z H); cases H (LExy Axy);
-    lapply (mtineq ?? x y z) as H1; whd in Axy; cases Axy (H2 H2); [cases (LExy H2)]
+    [1: apply (Le≫ ? (msymmetric ????)); assumption
+    |2: apply (Ap≫ ? (msymmetric ????)); assumption]
+|3: simplify; intros (x y z H); elim H (LExy Axy);
+    lapply (mtineq ?? x y z) as H1; elim (ap2exc ??? Axy) (H2 H2); [cases (LExy H2)]
     clear LExy; lapply (lt_le_transitive ???? H H1) as LT0;
     apply (lt0plus_orlt ????? LT0); apply mpositive;]
 qed.
     
-(* coercion cic:/matita/metric_space/apart_of_metric_space.con. *)
-
 lemma ap2delta: ∀R.∀m:metric_space R.∀x,y:m.ap_apart (apart_of_metric_space ? m) x y → 0 < δ x y.
 intros 2 (R m); cases m 0; simplify; intros; assumption; qed. 
diff --git a/helm/software/matita/dama/ordered_group.ma b/helm/software/matita/dama/ordered_group.ma
index 8677e755b..44529cadf 100644
--- a/helm/software/matita/dama/ordered_group.ma
+++ b/helm/software/matita/dama/ordered_group.ma
@@ -19,14 +19,14 @@ include "group.ma".
 record pogroup_ : Type ≝ { 
   og_abelian_group_: abelian_group;
   og_excess:> excess;
-  og_with: carr og_abelian_group_ = apart_of_excess og_excess
+  og_with: carr og_abelian_group_ = exc_ap og_excess
 }.
 
 lemma og_abelian_group: pogroup_ → abelian_group.
-intro G; apply (mk_abelian_group G); [1,2,3: rewrite < (og_with G)]
-[apply (plus (og_abelian_group_ G));|apply zero;|apply opp]
-unfold apartness_OF_pogroup_; cases (og_with G); simplify;
-[apply plus_assoc|apply plus_comm|apply zero_neutral|apply opp_inverse|apply plus_strong_ext]
+intro G; apply (mk_abelian_group G); unfold apartness_OF_pogroup_;
+cases (og_with G); simplify;
+[apply (plus (og_abelian_group_ G));|apply zero;|apply opp
+|apply plus_assoc|apply plus_comm|apply zero_neutral|apply opp_inverse|apply plus_strong_ext]
 qed.
 
 coercion cic:/matita/ordered_group/og_abelian_group.con.
diff --git a/helm/software/matita/dama/sandwich.ma b/helm/software/matita/dama/sandwich.ma
index 47709bd24..0ab83082e 100644
--- a/helm/software/matita/dama/sandwich.ma
+++ b/helm/software/matita/dama/sandwich.ma
@@ -26,22 +26,14 @@ lemma ltwr: ∀a,b,c:nat. a + b < c → a < c.
 intros 3 (x y z); rewrite > sym_plus; apply ltwl;
 qed. 
 
-include "sequence.ma".
-include "metric_lattice.ma".
-
-definition d2s ≝ 
-  λR.λml:mlattice R.λs:sequence ml.λk.λn. δ (s n) k.
-
-notation "s ⇝ x" non associative with precedence 50 for @{'tends $s $x}.
-  
-interpretation "tends to" 'tends s x = 
-  (cic:/matita/sequence/tends0.con _ (cic:/matita/sandwich/d2s.con _ _ s x)).
+include "tend.ma".
 
+alias symbol "leq" = "ordered sets less or equal than".
+alias symbol "and" = "constructive and".
 theorem sandwich:
 let ugo ≝ excess_OF_lattice1 in
   ∀R.∀ml:mlattice R.∀an,bn,xn:sequence ml.∀x:ml.
-    (∀n. (le (excess_OF_lattice1 ml) (xn n) (an n)) ∧ 
-     (le (excess_OF_lattice1 ?) (bn n) (xn n))) → True. 
+    (∀n. (xn n ≤ an n) ∧ (bn n ≤ xn n)) →  
     an ⇝ x → bn ⇝ x → xn ⇝ x.
 intros (R ml an bn xn x H Ha Hb); 
 unfold tends0 in Ha Hb ⊢ %; unfold d2s in Ha Hb ⊢ %; intros (e He);
diff --git a/helm/software/matita/dama/sandwich_corollary.ma b/helm/software/matita/dama/sandwich_corollary.ma
index 72da08236..6b509a4a8 100644
--- a/helm/software/matita/dama/sandwich_corollary.ma
+++ b/helm/software/matita/dama/sandwich_corollary.ma
@@ -14,15 +14,9 @@
 
 include "sandwich.ma".
 
-include "metric_lattice.ma".
-
 (* 3.17 *)
 lemma tends_uniq:
-  ∀R.∀ml:mlattice R.∀xn:sequence ml.
-  ∀x,y:ml. 
-  (* BUG: it inserts a compesoed coercion instead of an hand made one, 
-     what to do? prefer the human made one or allow to kill a coercion? 
-   *)
+  ∀R.∀ml:mlattice R.∀xn:sequence ml.∀x,y:ml. 
      xn ⇝ x → xn ⇝ y → δ x y ≈ 0.
 intros (R ml xn x y H1 H2); unfold tends0 in H1 H2; unfold d2s in H1 H2;
 intro Axy; lapply (ap_le_to_lt ??? (ap_symmetric ??? Axy) (mpositive ? ml ??)) as ge0;
diff --git a/helm/software/matita/dama/sequence.ma b/helm/software/matita/dama/sequence.ma
index 7536901ba..5a3e0ea1c 100644
--- a/helm/software/matita/dama/sequence.ma
+++ b/helm/software/matita/dama/sequence.ma
@@ -12,224 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
-
-
 include "excess.ma".
 
 definition sequence := λO:excess.nat → O.
 
-definition fun_of_sequence: ∀O:excess.sequence O → nat → O.
-intros; apply s; assumption;
-qed.
+definition fun_of_sequence: ∀O:excess.sequence O → nat → O ≝ λO.λx:sequence O.x.
 
 coercion cic:/matita/sequence/fun_of_sequence.con 1.
-
-definition upper_bound ≝ 
-  λO:excess.λa:sequence O.λu:O.∀n:nat.a n ≤ u.
-  
-definition lower_bound ≝ 
-  λO:excess.λa:sequence O.λu:O.∀n:nat.u ≤ a n.
-
-definition strong_sup ≝
-  λO:excess.λs:sequence O.λx.
-    upper_bound ? s x ∧ (∀y:O.x ≰ y → ∃n.s n ≰ y).
-  
-definition strong_inf ≝
-  λO:excess.λs:sequence O.λx.
-    lower_bound ? s x ∧ (∀y:O.y ≰ x → ∃n.y ≰ s n).
-
-definition weak_sup ≝
-  λO:excess.λs:sequence O.λx.
-    upper_bound ? s x ∧ (∀y:O.upper_bound ? s y → x ≤ y).
-  
-definition weak_inf ≝
-  λO:excess.λs:sequence O.λx.
-    lower_bound ? s x ∧ (∀y:O.lower_bound ? s y → y ≤ x).
-
-lemma strong_sup_is_weak: 
-  ∀O:excess.∀s:sequence O.∀x:O.strong_sup ? s x → weak_sup ? s x.
-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.
- 
-lemma strong_inf_is_weak: 
-  ∀O:excess.∀s:sequence O.∀x:O.strong_inf ? s x → weak_inf ? s x.
-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 tends0 ≝ 
-  λO:pogroup.λs:sequence O.
-    ∀e:O.0 < e → ∃N.∀n.N < n → -e < s n ∧ s n < e.
-    
-definition increasing ≝ 
-  λO:excess.λa:sequence O.∀n:nat.a n ≤ a (S n).
-
-definition decreasing ≝ 
-  λO:excess.λa:sequence O.∀n:nat.a (S n) ≤ a n.
-
-
-
-
-(*
-
-definition is_upper_bound ≝ λO:excess.λa:sequence O.λu:O.∀n:nat.a n ≤ u.
-definition is_lower_bound ≝ λO:excess.λa:sequence O.λu:O.∀n:nat.u ≤ a n.
-
-record is_sup (O:excess) (a:sequence O) (u:O) : Prop ≝
- { sup_upper_bound: is_upper_bound O a u; 
-   sup_least_upper_bound: ∀v:O. is_upper_bound O a v → u≤v
- }.
-
-record is_inf (O:excess) (a:sequence O) (u:O) : Prop ≝
- { inf_lower_bound: is_lower_bound O a u; 
-   inf_greatest_lower_bound: ∀v:O. is_lower_bound O a v → v≤u
- }.
-
-record is_bounded_below (O:excess) (a:sequence O) : Type ≝
- { ib_lower_bound: O;
-   ib_lower_bound_is_lower_bound: is_lower_bound ? a ib_lower_bound
- }.
-
-record is_bounded_above (O:excess) (a:sequence O) : Type ≝
- { ib_upper_bound: O;
-   ib_upper_bound_is_upper_bound: is_upper_bound ? a ib_upper_bound
- }.
-
-record is_bounded (O:excess) (a:sequence O) : Type ≝
- { ib_bounded_below:> is_bounded_below ? a;
-   ib_bounded_above:> is_bounded_above ? a
- }.
-
-record bounded_below_sequence (O:excess) : Type ≝
- { bbs_seq:> sequence O;
-   bbs_is_bounded_below:> is_bounded_below ? bbs_seq
- }.
-
-record bounded_above_sequence (O:excess) : Type ≝
- { bas_seq:> sequence O;
-   bas_is_bounded_above:> is_bounded_above ? bas_seq
- }.
-
-record bounded_sequence (O:excess) : Type ≝
- { bs_seq:> sequence O;
-   bs_is_bounded_below: is_bounded_below ? bs_seq;
-   bs_is_bounded_above: is_bounded_above ? bs_seq
- }.
-
-definition bounded_below_sequence_of_bounded_sequence ≝
- λO:excess.λb:bounded_sequence O.
-  mk_bounded_below_sequence ? b (bs_is_bounded_below ? b).
-
-coercion cic:/matita/sequence/bounded_below_sequence_of_bounded_sequence.con.
-
-definition bounded_above_sequence_of_bounded_sequence ≝
- λO:excess.λb:bounded_sequence O.
-  mk_bounded_above_sequence ? b (bs_is_bounded_above ? b).
-
-coercion cic:/matita/sequence/bounded_above_sequence_of_bounded_sequence.con.
-
-definition lower_bound ≝
- λO:excess.λb:bounded_below_sequence O.
-  ib_lower_bound ? b (bbs_is_bounded_below ? b).
-
-lemma lower_bound_is_lower_bound:
- ∀O:excess.∀b:bounded_below_sequence O.
-  is_lower_bound ? b (lower_bound ? b).
-intros; unfold lower_bound; apply ib_lower_bound_is_lower_bound.
-qed.
-
-definition upper_bound ≝
- λO:excess.λb:bounded_above_sequence O.
-  ib_upper_bound ? b (bas_is_bounded_above ? b).
-
-lemma upper_bound_is_upper_bound:
- ∀O:excess.∀b:bounded_above_sequence O.
-  is_upper_bound ? b (upper_bound ? b).
-intros; unfold upper_bound; apply ib_upper_bound_is_upper_bound.
-qed.
-
-definition reverse_excess: excess → excess.
-intros (E); apply (mk_excess E); [apply (λx,y.exc_relation E y x)] 
-cases E (T f cRf cTf); simplify; 
-[1: unfold Not; intros (x H); apply (cRf x); assumption
-|2: intros (x y z); apply Or_symmetric; apply cTf; assumption;]
-qed. 
-
-definition reverse_excess: excess → excess.
-intros (p); apply (mk_excess (reverse_excess p));
-generalize in match (reverse_excess p); intros (E);
-apply mk_is_porder_relation;
-[apply le_reflexive|apply le_transitive|apply le_antisymmetric]
-qed. 
- 
-lemma is_lower_bound_reverse_is_upper_bound:
- ∀O:excess.∀a:sequence O.∀l:O.
-  is_lower_bound O a l → is_upper_bound (reverse_excess O) a l.
-intros (O a l H); unfold; intros (n); unfold reverse_excess;
-unfold reverse_excess; simplify; fold unfold le (le ? l (a n)); apply H;    
-qed.
-
-lemma is_upper_bound_reverse_is_lower_bound:
- ∀O:excess.∀a:sequence O.∀l:O.
-  is_upper_bound O a l → is_lower_bound (reverse_excess O) a l.
-intros (O a l H); unfold; intros (n); unfold reverse_excess;
-unfold reverse_excess; simplify; fold unfold le (le ? (a n) l); apply H;    
-qed.
-
-lemma reverse_is_lower_bound_is_upper_bound:
- ∀O:excess.∀a:sequence O.∀l:O.
-  is_lower_bound (reverse_excess O) a l → is_upper_bound O a l.
-intros (O a l H); unfold; intros (n); unfold reverse_excess in H;
-unfold reverse_excess in H; simplify in H; apply H;    
-qed.
-
-lemma reverse_is_upper_bound_is_lower_bound:
- ∀O:excess.∀a:sequence O.∀l:O.
-  is_upper_bound (reverse_excess O) a l → is_lower_bound O a l.
-intros (O a l H); unfold; intros (n); unfold reverse_excess in H;
-unfold reverse_excess in H; simplify in H; apply H;    
-qed.
-
-lemma is_inf_to_reverse_is_sup:
- ∀O:excess.∀a:bounded_below_sequence O.∀l:O.
-  is_inf O a l → is_sup (reverse_excess O) a l.
-intros (O a l H); apply (mk_is_sup (reverse_excess O));
-[1: apply is_lower_bound_reverse_is_upper_bound; apply inf_lower_bound; assumption
-|2: unfold reverse_excess; simplify; unfold reverse_excess; simplify; 
-    intros (m H1); apply (inf_greatest_lower_bound ? ? ? H); apply H1;]
-qed.
-
-lemma is_sup_to_reverse_is_inf:
- ∀O:excess.∀a:bounded_above_sequence O.∀l:O.
-  is_sup O a l → is_inf (reverse_excess O) a l.
-intros (O a l H); apply (mk_is_inf (reverse_excess O));
-[1: apply is_upper_bound_reverse_is_lower_bound; apply sup_upper_bound; assumption
-|2: unfold reverse_excess; simplify; unfold reverse_excess; simplify; 
-    intros (m H1); apply (sup_least_upper_bound ? ? ? H); apply H1;]
-qed.
-
-lemma reverse_is_sup_to_is_inf:
- ∀O:excess.∀a:bounded_above_sequence O.∀l:O.
-  is_sup (reverse_excess O) a l → is_inf O a l.
-intros (O a l H); apply mk_is_inf;
-[1: apply reverse_is_upper_bound_is_lower_bound; 
-    apply (sup_upper_bound (reverse_excess O)); assumption
-|2: intros (v H1); apply (sup_least_upper_bound (reverse_excess O) a l H v);
-    apply is_lower_bound_reverse_is_upper_bound; assumption;]
-qed.
-
-lemma reverse_is_inf_to_is_sup:
- ∀O:excess.∀a:bounded_above_sequence O.∀l:O.
-  is_inf (reverse_excess O) a l → is_sup O a l.
-intros (O a l H); apply mk_is_sup;
-[1: apply reverse_is_lower_bound_is_upper_bound; 
-    apply (inf_lower_bound (reverse_excess O)); assumption
-|2: intros (v H1); apply (inf_greatest_lower_bound (reverse_excess O) a l H v);
-    apply is_upper_bound_reverse_is_lower_bound; assumption;]
-qed.
-
-*)
\ No newline at end of file
diff --git a/helm/software/matita/dama/tend.ma b/helm/software/matita/dama/tend.ma
new file mode 100644
index 000000000..d2decf0dc
--- /dev/null
+++ b/helm/software/matita/dama/tend.ma
@@ -0,0 +1,28 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "sequence.ma".
+include "metric_lattice.ma". (* we should probably use something weaker *)
+include "nat/orders.ma".
+
+definition tends0 ≝ 
+  λO:pogroup.λs:sequence O.∀e:O.0 < e → ∃N.∀n.N < n → -e < s n ∧ s n < e.
+
+definition d2s ≝ 
+  λR.λml:mlattice R.λs:sequence ml.λk.λn. δ (s n) k.
+
+notation "s ⇝ x" non associative with precedence 50 for @{'tends $s $x}.
+interpretation "tends to" 'tends s x = 
+  (cic:/matita/tend/tends0.con _ (cic:/matita/tend/d2s.con _ _ s x)).
+
-- 
2.39.2