From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 20 Nov 2008 16:06:24 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~4525
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9bcbaf15316cfb7fbe831af1efb89da954f40b72;p=helm.git

...
---

diff --git a/helm/software/matita/contribs/dama/dama/bishop_set.ma b/helm/software/matita/contribs/dama/dama/bishop_set.ma
deleted file mode 100644
index d69bb2732..000000000
--- a/helm/software/matita/contribs/dama/dama/bishop_set.ma
+++ /dev/null
@@ -1,89 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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 "ordered_set.ma".
-
-(* Definition 2.2, setoid *)
-record bishop_set: Type ≝ {
-  bs_carr:> Type;
-  bs_apart: bs_carr → bs_carr → CProp;
-  bs_coreflexive: coreflexive ? bs_apart;
-  bs_symmetric: symmetric ? bs_apart;
-  bs_cotransitive: cotransitive ? bs_apart
-}.
-
-interpretation "bishop set apartness" 'apart x y = (bs_apart _ x y).
-
-definition bishop_set_of_ordered_set: ordered_set → bishop_set.
-intros (E); apply (mk_bishop_set E (λa,b:E. a ≰ b ∨ b ≰ a));  
-[1: intro x; simplify; intro H; cases H; clear H;
-    apply (exc_coreflexive x H1);
-|2: intros 3 (x y H); simplify in H ⊢ %; cases H; [right|left]assumption; 
-|3: intros 4 (x y z H);  simplify in H ⊢ %; cases H; clear H;
-    [ cases (exc_cotransitive x y z H1); [left;left|right;left] assumption;
-    | cases (exc_cotransitive y x z H1); [right;right|left;right] assumption;]]
-qed.
-
-(* Definition 2.2 (2) *)
-definition eq ≝ λA:bishop_set.λa,b:A. ¬ (a # b).
-
-interpretation "Bishop set alikeness" 'napart a b = (eq _ a b). 
-
-lemma eq_reflexive:∀E:bishop_set. reflexive ? (eq E).
-intros (E); unfold; intros (x); apply bs_coreflexive; 
-qed.
-
-lemma eq_sym_:∀E:bishop_set.symmetric ? (eq E).
-intros 4 (E x y H); intro T; cases (H (bs_symmetric ??? T)); 
-qed.
-
-lemma eq_sym:∀E:bishop_set.∀x,y:E.x ≈ y → y ≈ x ≝ eq_sym_.
-
-lemma eq_trans_: ∀E:bishop_set.transitive ? (eq E).
-intros 6 (E x y z Exy Eyz); intro Axy; cases (bs_cotransitive ???y Axy); 
-[apply Exy|apply Eyz] assumption.
-qed.
-
-coercion bishop_set_of_ordered_set.
-
-lemma le_antisymmetric: 
-  ∀E:ordered_set.antisymmetric E (le (os_l E)) (eq E).
-intros 5 (E x y Lxy Lyx); intro H; 
-cases H; [apply Lxy;|apply Lyx] assumption;
-qed.
-
-lemma le_le_eq: ∀E:ordered_set.∀a,b:E. a ≤ b → b ≤ a → a ≈ b.
-intros (E x y L1 L2); intro H; cases H; [apply L1|apply L2] assumption;
-qed.
-
-definition bs_subset ≝ λO:bishop_set.λP,Q:O→Prop.∀x:O.P x → Q x.
-
-interpretation "bishop set subset" 'subseteq a b = (bs_subset _ a b). 
-
-definition square_bishop_set : bishop_set → bishop_set.
-intro S; apply (mk_bishop_set (S × S));
-[1: intros (x y); apply ((\fst x # \fst y) ∨ (\snd x # \snd y));
-|2: intro x; simplify; intro; cases H (X X); clear H; apply (bs_coreflexive ?? X);   
-|3: intros 2 (x y); simplify; intro H; cases H (X X); clear H; [left|right] apply (bs_symmetric ??? X); 
-|4: intros 3 (x y z); simplify; intro H; cases H (X X); clear H;
-    [1: cases (bs_cotransitive ??? (\fst z) X); [left;left|right;left]assumption;
-    |2: cases (bs_cotransitive ??? (\snd z) X); [left;right|right;right]assumption;]]
-qed.
-
-notation "s 2 \atop \neq" non associative with precedence 90
-  for @{ 'square_bs $s }.
-notation > "s 'squareB'" non associative with precedence 90
-  for @{ 'squareB $s }.
-interpretation "bishop set square" 'squareB x = (square_bishop_set x).
-interpretation "bishop set square" 'square_bs x = (square_bishop_set x).
\ No newline at end of file
diff --git a/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma b/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma
deleted file mode 100644
index ff063e29a..000000000
--- a/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma
+++ /dev/null
@@ -1,87 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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 "bishop_set.ma".
-
-coercion eq_sym.
-
-lemma eq_trans:∀E:bishop_set.∀x,z,y:E.x ≈ y → y ≈ z → x ≈ z ≝ 
-  λE,x,y,z.eq_trans_ E x z y.
-
-notation > "'Eq'≈" non associative with precedence 50 
-  for @{'eqrewrite}.
-  
-interpretation "eq_rew" 'eqrewrite = (eq_trans _ _ _).
-
-lemma le_rewl: ∀E:ordered_set.∀z,y,x:E. x ≈ y → x ≤ z → y ≤ z.
-intros (E z y x Exy Lxz); apply (le_transitive ??? ? Lxz);
-intro Xyz; apply Exy; right; assumption;
-qed.
-
-lemma le_rewr: ∀E:ordered_set.∀z,y,x:E. x ≈ y → z ≤ x → z ≤ y.
-intros (E z y x Exy Lxz); apply (le_transitive ??? Lxz);
-intro Xyz; apply Exy; left; assumption;
-qed.
-
-notation > "'Le'≪" non associative with precedence 50 for @{'lerewritel}.
-interpretation "le_rewl" 'lerewritel = (le_rewl _ _ _).
-notation > "'Le'≫" non associative with precedence 50 for @{'lerewriter}.
-interpretation "le_rewr" 'lerewriter = (le_rewr _ _ _).
-
-lemma ap_rewl: ∀A:bishop_set.∀x,z,y:A. x ≈ y → y # z → x # z.
-intros (A x z y Exy Ayz); cases (bs_cotransitive ???x Ayz); [2:assumption]
-cases (eq_sym ??? Exy H);
-qed.
-  
-lemma ap_rewr: ∀A:bishop_set.∀x,z,y:A. x ≈ y → z # y → z # x.
-intros (A x z y Exy Azy); apply bs_symmetric; apply (ap_rewl ???? Exy);
-apply bs_symmetric; assumption;
-qed.
-
-notation > "'Ap'≪" non associative with precedence 50 for @{'aprewritel}.
-interpretation "ap_rewl" 'aprewritel = (ap_rewl _ _ _).
-notation > "'Ap'≫" non associative with precedence 50 for @{'aprewriter}.
-interpretation "ap_rewr" 'aprewriter = (ap_rewr _ _ _).
-
-lemma exc_rewl: ∀A:ordered_set.∀x,z,y:A. x ≈ y → y ≰ z → x ≰ z.
-intros (A x z y Exy Ayz); cases (exc_cotransitive ?? x Ayz); [2:assumption]
-cases Exy; right; assumption;
-qed.
-  
-lemma exc_rewr: ∀A:ordered_set.∀x,z,y:A. x ≈ y → z ≰ y → z ≰ x.
-intros (A x z y Exy Azy); cases (exc_cotransitive ??x Azy); [assumption]
-cases (Exy); left; assumption;
-qed.
-
-notation > "'Ex'≪" non associative with precedence 50 for @{'ordered_setrewritel}.
-interpretation "exc_rewl" 'ordered_setrewritel = (exc_rewl _ _ _).
-notation > "'Ex'≫" non associative with precedence 50 for @{'ordered_setrewriter}.
-interpretation "exc_rewr" 'ordered_setrewriter = (exc_rewr _ _ _).
-
-(*
-lemma lt_rewr: ∀A:ordered_set.∀x,z,y:A. x ≈ y → z < y → z < x.
-intros (A x y z E H); split; cases H;
-[apply (Le≫ ? (eq_sym ??? E));|apply (Ap≫ ? E)] assumption;
-qed.
-
-lemma lt_rewl: ∀A:ordered_set.∀x,z,y:A. x ≈ y → y < z → x < z.
-intros (A x y z E H); split; cases H;
-[apply (Le≪ ? (eq_sym ??? E));| apply (Ap≪ ? E);] assumption;
-qed.
-
-notation > "'Lt'≪" non associative with precedence 50 for @{'ltrewritel}.
-interpretation "lt_rewl" 'ltrewritel = (lt_rewl _ _ _).
-notation > "'Lt'≫" non associative with precedence 50 for @{'ltrewriter}.
-interpretation "lt_rewr" 'ltrewriter = (lt_rewr _ _ _).
-*)
diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends
index 7e0d8968e..68f26f5b4 100644
--- a/helm/software/matita/contribs/dama/dama/depends
+++ b/helm/software/matita/contribs/dama/dama/depends
@@ -1,35 +1,13 @@
-property_exhaustivity.ma ordered_uniform.ma property_sigma.ma
-sequence.ma nat/nat.ma
-supremum.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma sequence.ma
-bishop_set_rewrite.ma bishop_set.ma
-property_sigma.ma ordered_uniform.ma russell_support.ma
 models/q_support.ma Q/q/qplus.ma Q/q/qtimes.ma logic/cprop_connectives.ma
-models/increasing_supremum_stabilizes.ma models/nat_uniform.ma nat/le_arith.ma russell_support.ma supremum.ma
-ordered_set.ma datatypes/constructors.ma logic/cprop_connectives.ma
-sandwich.ma ordered_uniform.ma
-nat_ordered_set.ma bishop_set.ma nat/compare.ma
-models/nat_ordered_uniform.ma bishop_set_rewrite.ma models/nat_uniform.ma ordered_uniform.ma
+models/q_bars.ma dama/nat_ordered_set.ma logic/cprop_connectives.ma models/list_support.ma models/q_support.ma
 models/list_support.ma list/list.ma logic/cprop_connectives.ma nat/minus.ma
-models/q_bars.ma logic/cprop_connectives.ma models/list_support.ma models/q_support.ma nat_ordered_set.ma
 .unnamed.ma 
-lebesgue.ma ordered_set.ma property_exhaustivity.ma sandwich.ma
-bishop_set.ma ordered_set.ma
-models/nat_order_continuous.ma models/increasing_supremum_stabilizes.ma models/nat_ordered_uniform.ma
-models/discrete_uniformity.ma bishop_set_rewrite.ma uniform.ma
-russell_support.ma logic/cprop_connectives.ma nat/nat.ma
 models/q_copy.ma models/q_bars.ma
-models/nat_lebesgue.ma lebesgue.ma models/nat_order_continuous.ma
-models/nat_uniform.ma models/discrete_uniformity.ma nat_ordered_set.ma
-ordered_uniform.ma uniform.ma
-uniform.ma supremum.ma
-models/q_rebase.ma Q/q/qtimes.ma models/q_copy.ma russell_support.ma
+models/q_rebase.ma Q/q/qtimes.ma dama/russell_support.ma models/q_copy.ma
 Q/q/qplus.ma 
 Q/q/qtimes.ma 
-datatypes/constructors.ma 
+dama/nat_ordered_set.ma 
+dama/russell_support.ma 
 list/list.ma 
 logic/cprop_connectives.ma 
-nat/compare.ma 
-nat/le_arith.ma 
 nat/minus.ma 
-nat/nat.ma 
-nat/plus.ma 
diff --git a/helm/software/matita/contribs/dama/dama/depends.png b/helm/software/matita/contribs/dama/dama/depends.png
index 1c10c2366..f562abce0 100644
Binary files a/helm/software/matita/contribs/dama/dama/depends.png and b/helm/software/matita/contribs/dama/dama/depends.png differ
diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma
deleted file mode 100644
index f81c5ce46..000000000
--- a/helm/software/matita/contribs/dama/dama/lebesgue.ma
+++ /dev/null
@@ -1,125 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* manca un pezzo del pullback, se inverto poi non tipa *)
-include "sandwich.ma".
-include "property_exhaustivity.ma".
-
-(* NOT DUALIZED *)
-alias symbol "low" = "lower".
-alias id "le" = "cic:/matita/dama/ordered_set/le.con".
-lemma order_converges_bigger_lowsegment:
-  ∀C:ordered_set.
-   ∀a:sequence (os_l C).∀s:segment C.∀H:∀i:nat.a i ∈ s. 
-     ∀x:C.∀p:order_converge C a x. 
-       ∀j. 𝕝_s ≤ (pi1exT23 ???? p j).
-intros; cases p (xi yi Ux Dy Hxy); clear p; simplify; 
-cases Ux (Ixi Sxi); clear Ux; cases Dy (Dyi Iyi); clear Dy;
-cases (Hxy j) (Ia Sa); clear Hxy; cases Ia (Da SSa); cases Sa (Inca SIa); clear Ia Sa;
-intro H2; cases (SSa 𝕝_s H2) (w Hw); simplify in Hw;
-lapply (H (w+j)) as K; cases (cases_in_segment ? s ? K); apply H3; apply Hw;
-qed.   
-  
-alias symbol "upp" = "uppper".
-alias symbol "leq" = "Ordered set less or equal than".
-lemma order_converges_smaller_upsegment:
-  ∀C:ordered_set.
-   ∀a:sequence (os_l C).∀s:segment C.∀H:∀i:nat.a i ∈ s. 
-     ∀x:C.∀p:order_converge C a x. 
-       ∀j. (pi2exT23 ???? p j) ≤ 𝕦_s.
-intros; cases p (xi yi Ux Dy Hxy); clear p; simplify; 
-cases Ux (Ixi Sxi); clear Ux; cases Dy (Dyi Iyi); clear Dy;
-cases (Hxy j) (Ia Sa); clear Hxy; cases Ia (Da SSa); cases Sa (Inca SIa); clear Ia Sa;
-intro H2; cases (SIa 𝕦_s H2) (w Hw); lapply (H (w+j)) as K; 
-cases (cases_in_segment ? s ? K); apply H1; apply Hw;  
-qed. 
-
-(* Theorem 3.10 *)
-theorem lebesgue_oc:
-  ∀C:ordered_uniform_space.
-   (∀s:‡C.order_continuity {[s]}) →
-    ∀a:sequence C.∀s:‡C.∀H:∀i:nat.a i ∈ s. 
-     ∀x:C.a order_converges x → 
-      x ∈ s ∧ 
-      ∀h:x ∈ s.
-       uniform_converge {[s]} (⌊n,≪a n,H n≫⌋) ≪x,h≫.
-intros; 
-generalize in match (order_converges_bigger_lowsegment ? a s H1 ? H2);
-generalize in match (order_converges_smaller_upsegment ? a s H1 ? H2);
-cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ ((?→???%) → (?→???%) → ?); intros;
-cut (∀i.xi i ∈ s) as Hxi; [2:
-  intros; apply (prove_in_segment (os_l C)); [apply (H3 i)] cases (Hxy i) (H5 _); cases H5 (H7 _);
-  lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu);
-  simplify in K:(? ? % ?); apply (hle_transitive (os_l C) (xi i) (a i) 𝕦_s K Pu);] clear H3;
-cut (∀i.yi i ∈ s) as Hyi; [2:
-  intros; apply (prove_in_segment (os_l C)); [2:apply (H2 i)] cases (Hxy i) (_ H5); cases H5 (H7 _);
-  lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu); simplify in K;
-  apply (le_transitive 𝕝_s ? ? ? K);apply Pl;] clear H2;
-split;
-[1: apply (uparrow_to_in_segment s ? Hxi ? Hx);
-|2: intros 3 (h);
-    letin Xi ≝ (⌊n,≪xi n, Hxi n≫⌋);
-    letin Yi ≝ (⌊n,≪yi n, Hyi n≫⌋);
-    letin Ai ≝ (⌊n,≪a n, H1 n≫⌋); 
-    apply (sandwich {[s]} ≪x, h≫ Xi Yi Ai); [4: assumption;]
-    [1: intro j; cases (Hxy j); cases H3; cases H4; split; clear H3 H4; simplify in H5 H7;
-        [apply (l2sl_ ? s (Xi j) (Ai j) (H5 0));|apply (l2sl_ ? s (Ai j) (Yi j) (H7 0))]
-    |2: cases (H s Xi ≪?,h≫) (Ux Uy); apply Ux; cases Hx; split; [intro i; apply (l2sl_ ? s (Xi i) (Xi (S i)) (H3 i));]
-        cases H4; split; [intro i; apply (l2sl_ ? s (Xi i) ≪x,h≫ (H5 i))] 
-        intros (y Hy);cases (H6 (\fst y));[2:apply (sx2x_ ? s ? y Hy)]
-        exists [apply w] apply (x2sx_ ? s (Xi w) y H7); 
-    |3: cases (H s Yi ≪?,h≫) (Ux Uy); apply Uy; cases Hy; split; [intro i; apply (l2sl_ ? s (Yi (S i))  (Yi i) (H3 i));]
-        cases H4; split; [intro i; apply (l2sl_ ? s ≪x,h≫ (Yi i) (H5 i))]
-        intros (y Hy);cases (H6 (\fst y));[2:apply (sx2x_ ? s y ≪x,h≫ Hy)]
-        exists [apply w] apply (x2sx_ ? s y (Yi w) H7);]]
-qed.
- 
-
-(* Theorem 3.9 *)
-theorem lebesgue_se:
-  ∀C:ordered_uniform_space.property_sigma C →
-   (∀s:‡C.exhaustive {[s]}) →
-    ∀a:sequence C.∀s:‡C.∀H:∀i:nat.a i ∈ s. 
-     ∀x:C.a order_converges x → 
-      x ∈ s ∧ 
-      ∀h:x ∈ s.
-       uniform_converge {[s]} (⌊n,≪a n,H n≫⌋) ≪x,h≫.
-intros (C S);
-generalize in match (order_converges_bigger_lowsegment ? a s H1 ? H2);
-generalize in match (order_converges_smaller_upsegment ? a s H1 ? H2);
-cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ ((?→???%) → (?→???%) → ?); intros;
-cut (∀i.xi i ∈ s) as Hxi; [2:
-  intros; apply (prove_in_segment (os_l C)); [apply (H3 i)] cases (Hxy i) (H5 _); cases H5 (H7 _);
-  lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu);
-  simplify in K:(? ? % ?); apply (hle_transitive (os_l C) (xi i) (a i) 𝕦_s K Pu);] clear H3;
-cut (∀i.yi i ∈ s) as Hyi; [2:
-  intros; apply (prove_in_segment (os_l C)); [2:apply (H2 i)] cases (Hxy i) (_ H5); cases H5 (H7 _);
-  lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu); simplify in K;
-  apply (le_transitive 𝕝_s ? ? ? K);apply Pl;] clear H2;
-letin Xi ≝ (⌊n,≪xi n, Hxi n≫⌋);
-letin Yi ≝ (⌊n,≪yi n, Hyi n≫⌋);
-cases (restrict_uniform_convergence_uparrow ? S ? (H s) Xi x Hx);
-cases (restrict_uniform_convergence_downarrow ? S ? (H s) Yi x Hy);
-split; [1: assumption]
-intros 3;
-lapply (uparrow_upperlocated  xi x Hx)as Ux;
-lapply (downarrow_lowerlocated  yi x Hy)as Uy;
-letin Ai ≝ (⌊n,≪a n, H1 n≫⌋);
-apply (sandwich {[s]} ≪x, h≫ Xi Yi Ai); [4: assumption;|2:apply H3;|3:apply H5]
-intro j; cases (Hxy j); cases H7; cases H8; split;
-[apply (l2sl_ ? s (Xi j) (Ai j) (H9 0));|apply (l2sl_ ? s (Ai j) (Yi j) (H11 0))]
-qed. 
-
-
-
diff --git a/helm/software/matita/contribs/dama/dama/models/q_bars.ma b/helm/software/matita/contribs/dama/dama/models/q_bars.ma
index 1d2107b7c..f3224e627 100644
--- a/helm/software/matita/contribs/dama/dama/models/q_bars.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_bars.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "nat_ordered_set.ma".
+include "dama/nat_ordered_set.ma".
 include "models/q_support.ma".
 include "models/list_support.ma". 
 include "logic/cprop_connectives.ma". 
diff --git a/helm/software/matita/contribs/dama/dama/models/q_rebase.ma b/helm/software/matita/contribs/dama/dama/models/q_rebase.ma
index f8243d6d1..b14f0bd17 100644
--- a/helm/software/matita/contribs/dama/dama/models/q_rebase.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_rebase.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "russell_support.ma".
+include "dama/russell_support.ma".
 include "models/q_copy.ma".
 (*
 definition rebase_spec ≝ 
diff --git a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
deleted file mode 100644
index 26e2f0d29..000000000
--- a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
+++ /dev/null
@@ -1,65 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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 "nat/compare.ma".
-include "bishop_set.ma". 
-
-definition nat_excess : nat → nat → CProp ≝ λn,m. m<n.
-
-lemma nat_elim2: 
-  ∀R:nat → nat → CProp.
-  (∀ n:nat. R O n) → (∀n:nat. R (S n) O) → (∀n,m:nat. R n m → R (S n) (S m)) →
-    ∀n,m:nat. R n m.
-intros 5;elim n; [apply H]
-cases m;[ apply H1| apply H2; apply H3 ]
-qed.
-
-alias symbol "lt" = "natural 'less than'".
-lemma nat_discriminable: ∀x,y:nat.x < y ∨ x = y ∨ y < x.
-intros (x y); apply (nat_elim2 ???? x y); 
-[1: intro;left;cases n; [right;reflexivity] left; apply lt_O_S;
-|2: intro;right;apply lt_O_S;
-|3: intros; cases H; 
-    [1: cases H1; [left; left; apply le_S_S; assumption]
-        left;right;rewrite > H2; reflexivity;
-    |2: right;apply le_S_S; assumption]]
-qed.
-        
-lemma nat_excess_cotransitive: cotransitive ? nat_excess.
-intros 3 (x y z); unfold nat_excess; simplify; intros;
-cases (nat_discriminable x z); [2: left; assumption] cases H1; clear H1;
-[1: right; apply (trans_lt ??? H H2);
-|2: right; rewrite < H2; assumption;]
-qed.
-  
-lemma nat_ordered_set : ordered_set.
-letin hos ≝ (mk_half_ordered_set nat (λT,R:Type.λf:T→T→R.f) ? nat_excess ? nat_excess_cotransitive);
-[ intros; left; intros; reflexivity;
-| intro x; intro H; apply (not_le_Sn_n ? H);]
-constructor 1;  apply hos;
-qed.
-
-interpretation "ordered set N" 'N = nat_ordered_set.
-
-alias id "le" = "cic:/matita/nat/orders/le.ind#xpointer(1/1)".
-lemma os_le_to_nat_le:
-  ∀a,b:nat_ordered_set.a ≤ b → le a b.
-intros; normalize in H; apply (not_lt_to_le b a H);
-qed.
- 
-lemma nat_le_to_os_le:
-  ∀a,b:nat_ordered_set.le a b → a ≤ b.
-intros 3; apply (le_to_not_lt a b);assumption;
-qed.
-
diff --git a/helm/software/matita/contribs/dama/dama/ordered_set.ma b/helm/software/matita/contribs/dama/dama/ordered_set.ma
deleted file mode 100644
index 890164ea9..000000000
--- a/helm/software/matita/contribs/dama/dama/ordered_set.ma
+++ /dev/null
@@ -1,181 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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 "datatypes/constructors.ma".
-include "logic/cprop_connectives.ma".
-
-
-(* TEMPLATES
-notation "''" non associative with precedence 90 for @{'}.
-notation "''" non associative with precedence 90 for @{'}.
-
-interpretation "" ' = ( (os_l _)).
-interpretation "" ' = ( (os_r _)).
-*)
-
-(* Definition 2.1 *)
-record half_ordered_set: Type ≝ {
-  hos_carr:> Type;
-  wloss: ∀A,B:Type. (A → A → B) → A → A → B;
-  wloss_prop: (∀T,R,P,x,y.P x y = wloss T R P x y) ∨ (∀T,R,P,x,y.P y x = wloss T R P x y); 
-  hos_excess_: hos_carr → hos_carr → CProp;
-  hos_coreflexive: coreflexive ? (wloss ?? hos_excess_);
-  hos_cotransitive: cotransitive ? (wloss ?? hos_excess_)
-}.
-
-definition hos_excess ≝ λO:half_ordered_set.wloss O ?? (hos_excess_ O). 
-
-definition dual_hos : half_ordered_set → half_ordered_set.
-intro; constructor 1;
-[ apply (hos_carr h);
-| apply (λT,R,f,x,y.wloss h T R f y x); 
-| intros; cases (wloss_prop h);[right|left]intros;apply H; 
-| apply (hos_excess_ h);
-| apply (hos_coreflexive h);
-| intros 4 (x y z H); simplify in H ⊢ %; cases (hos_cotransitive h y x z H);
-  [right|left] assumption;]
-qed.
-
-record ordered_set : Type ≝ {
-  os_l : half_ordered_set
-}.
-
-definition os_r : ordered_set → half_ordered_set.
-intro o; apply (dual_hos (os_l o)); qed.
-
-lemma half2full : half_ordered_set → ordered_set.
-intro hos;
-constructor 1; apply hos;  
-qed.
-
-definition Type_of_ordered_set : ordered_set → Type.
-intro o; apply (hos_carr (os_l o)); qed.
-
-definition Type_of_ordered_set_dual : ordered_set → Type.
-intro o; apply (hos_carr (os_r o)); qed.
-
-coercion Type_of_ordered_set_dual.
-coercion Type_of_ordered_set.
-
-notation "a ≰≰ b" non associative with precedence 45 for @{'nleq_low $a $b}.
-interpretation "Ordered half set excess" 'nleq_low a b = (hos_excess _ a b).
-
-interpretation "Ordered set excess (dual)" 'ngeq a b = (hos_excess (os_r _) a b).
-interpretation "Ordered set excess" 'nleq a b = (hos_excess (os_l _) a b).
-
-notation "'exc_coreflexive'" non associative with precedence 90 for @{'exc_coreflexive}.
-notation "'cxe_coreflexive'" non associative with precedence 90 for @{'cxe_coreflexive}.
-
-interpretation "exc_coreflexive" 'exc_coreflexive = ((hos_coreflexive (os_l _))).
-interpretation "cxe_coreflexive" 'cxe_coreflexive = ((hos_coreflexive (os_r _))).
-
-notation "'exc_cotransitive'" non associative with precedence 90 for @{'exc_cotransitive}.
-notation "'cxe_cotransitive'" non associative with precedence 90 for @{'cxe_cotransitive}.
-
-interpretation "exc_cotransitive" 'exc_cotransitive = ((hos_cotransitive (os_l _))).
-interpretation "cxe_cotransitive" 'cxe_cotransitive = ((hos_cotransitive (os_r _))).
-
-(* Definition 2.2 (3) *)
-definition le ≝ λE:half_ordered_set.λa,b:E. ¬ (a ≰≰ b).
-
-notation "hvbox(a break ≤≤ b)" non associative with precedence 45 for @{ 'leq_low $a $b }.
-interpretation "Half ordered set greater or equal than" 'leq_low a b = ((le _ a b)).
-
-interpretation "Ordered set greater or equal than" 'geq a b = ((le (os_r _) a b)).
-interpretation "Ordered set less or equal than" 'leq a b = ((le (os_l _) a b)).
-
-lemma hle_reflexive: ∀E.reflexive ? (le E).
-unfold reflexive; intros 3; apply (hos_coreflexive ? x H);
-qed.
-
-notation "'le_reflexive'" non associative with precedence 90 for @{'le_reflexive}.
-notation "'ge_reflexive'" non associative with precedence 90 for @{'ge_reflexive}.
-
-interpretation "le reflexive" 'le_reflexive = (hle_reflexive (os_l _)).
-interpretation "ge reflexive" 'ge_reflexive = (hle_reflexive (os_r _)).
-
-(* DUALITY TESTS 
-lemma test_le_ge_convertible :∀o:ordered_set.∀x,y:o. x ≤ y → y ≥ x.
-intros; assumption; qed.
-
-lemma test_ge_reflexive :∀o:ordered_set.∀x:o. x ≥ x.
-intros; apply ge_reflexive. qed.
-
-lemma test_le_reflexive :∀o:ordered_set.∀x:o. x ≤ x.
-intros; apply le_reflexive. qed.
-*)
-
-lemma hle_transitive: ∀E.transitive ? (le E).
-unfold transitive; intros 7 (E x y z H1 H2 H3); cases (hos_cotransitive E x z y H3) (H4 H4);
-[cases (H1 H4)|cases (H2 H4)]
-qed.
-
-notation "'le_transitive'" non associative with precedence 90 for @{'le_transitive}.
-notation "'ge_transitive'" non associative with precedence 90 for @{'ge_transitive}.
-
-interpretation "le transitive" 'le_transitive = (hle_transitive (os_l _)).
-interpretation "ge transitive" 'ge_transitive = (hle_transitive (os_r _)).
-
-(* Lemma 2.3 *)
-lemma exc_hle_variance: 
-  ∀O:half_ordered_set.∀a,b,a',b':O.a ≰≰ b → a ≤≤ a' → b' ≤≤ b → a' ≰≰ b'. 
-intros (O a b a1 b1 Eab Laa1 Lb1b);
-cases (hos_cotransitive ? a b a1 Eab) (H H); [cases (Laa1 H)]
-cases (hos_cotransitive ? ?? b1 H) (H1 H1); [assumption]
-cases (Lb1b H1);
-qed.
-
-notation "'exc_le_variance'" non associative with precedence 90 for @{'exc_le_variance}.
-notation "'exc_ge_variance'" non associative with precedence 90 for @{'exc_ge_variance}.
-
-interpretation "exc_le_variance" 'exc_le_variance = (exc_hle_variance (os_l _)).
-interpretation "exc_ge_variance" 'exc_ge_variance = (exc_hle_variance (os_r _)).
-
-definition square_exc ≝
- λO:half_ordered_set.λx,y:O×O.\fst x ≰≰ \fst y ∨ \snd x ≰≰ \snd y.
-
-lemma square_half_ordered_set: half_ordered_set → half_ordered_set.
-intro O;
-apply (mk_half_ordered_set (O × O));
-[1: apply (wloss O);
-|2: intros; cases (wloss_prop O); [left|right] intros; apply H;
-|3: apply (square_exc O); 
-|4: intro x; cases (wloss_prop O); rewrite < (H  ?? (square_exc O) x x); clear H;
-    cases x; clear x; unfold square_exc; intro H; cases H; clear H; simplify in H1;
-    [1,3: apply (hos_coreflexive O h H1);
-    |*: apply (hos_coreflexive O h1 H1);]
-|5: intros 3 (x0 y0 z0); cases (wloss_prop O);
-    do 3 rewrite < (H  ?? (square_exc O)); clear H; cases x0; cases y0; cases z0; clear x0 y0 z0;
-    simplify; intro H; cases H; clear H;
-    [1: cases (hos_cotransitive ? h h2 h4 H1); [left;left|right;left] assumption;
-    |2: cases (hos_cotransitive ? h1 h3 h5 H1); [left;right|right;right] assumption;
-    |3: cases (hos_cotransitive ? h2 h h4 H1); [right;left|left;left] assumption;
-    |4: cases (hos_cotransitive ? h3 h1 h5 H1); [right;right|left;right] assumption;]]
-qed.
-
-lemma square_ordered_set: ordered_set → ordered_set.
-intro O; constructor 1; apply (square_half_ordered_set (os_l O));
-qed.
-
-notation "s 2 \atop \nleq" non associative with precedence 90
-  for @{ 'square_os $s }.
-notation > "s 'squareO'" non associative with precedence 90
-  for @{ 'squareO $s }.
-interpretation "ordered set square" 'squareO s = (square_ordered_set s). 
-interpretation "ordered set square" 'square_os s = (square_ordered_set s).
-
-definition os_subset ≝ λO:ordered_set.λP,Q:O→Prop.∀x:O.P x → Q x.
-
-interpretation "ordered set subset" 'subseteq a b = (os_subset _ a b). 
-
diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
deleted file mode 100644
index 5a712f127..000000000
--- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
+++ /dev/null
@@ -1,243 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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 "uniform.ma".
-
-record ordered_uniform_space_ : Type ≝ {
-  ous_os:> ordered_set;
-  ous_us_: uniform_space;
-  with_ : us_carr ous_us_ = bishop_set_of_ordered_set ous_os
-}.
-
-lemma ous_unifspace: ordered_uniform_space_ → uniform_space.
-intro X; apply (mk_uniform_space (bishop_set_of_ordered_set X));
-unfold bishop_set_OF_ordered_uniform_space_;
-[1: rewrite < (with_ X); simplify; apply (us_unifbase (ous_us_ X));
-|2: cases (with_ X); simplify; apply (us_phi1 (ous_us_ X));
-|3: cases (with_ X); simplify; apply (us_phi2 (ous_us_ X));
-|4: cases (with_ X); simplify; apply (us_phi3 (ous_us_ X));
-|5: cases (with_ X); simplify; apply (us_phi4 (ous_us_ X))]
-qed.
-
-coercion ous_unifspace.
-
-record ordered_uniform_space : Type ≝ {
-  ous_stuff :> ordered_uniform_space_;
-  ous_convex_l: ∀U.us_unifbase ous_stuff U → convex (os_l ous_stuff) U;
-  ous_convex_r: ∀U.us_unifbase ous_stuff U → convex (os_r ous_stuff) U
-}.   
-
-definition half_ordered_set_OF_ordered_uniform_space : ordered_uniform_space → half_ordered_set.
-intro; compose ordered_set_OF_ordered_uniform_space with os_l. apply (f o);
-qed.
-
-definition invert_os_relation ≝
-  λC:ordered_set.λU:C squareO → Prop.
-    λx:C squareO. U 〈\snd x,\fst x〉.
-
-interpretation "relation invertion" 'invert a = (invert_os_relation _ a).
-interpretation "relation invertion" 'invert_symbol = (invert_os_relation _).
-interpretation "relation invertion" 'invert_appl a x = (invert_os_relation _ a x).
-
-lemma hint_segment: ∀O.
- segment (Type_of_ordered_set O) →
- segment (hos_carr (os_l O)).
-intros; assumption;
-qed.
-
-coercion hint_segment nocomposites.
-
-lemma segment_square_of_ordered_set_square: 
-  ∀O:ordered_set.∀s:‡O.∀x:O squareO.
-   \fst x ∈ s → \snd x ∈ s → {[s]} squareO.
-intros; split; exists; [1: apply (\fst x) |3: apply (\snd x)] assumption;
-qed.
-
-coercion segment_square_of_ordered_set_square with 0 2 nocomposites.
-
-alias symbol "pi1" (instance 4) = "exT \fst".
-alias symbol "pi1" (instance 2) = "exT \fst".
-lemma ordered_set_square_of_segment_square : 
- ∀O:ordered_set.∀s:‡O.{[s]} squareO → O squareO ≝ 
-  λO:ordered_set.λs:‡O.λb:{[s]} squareO.〈\fst(\fst b),\fst(\snd b)〉.
-
-coercion ordered_set_square_of_segment_square nocomposites.
-
-lemma restriction_agreement : 
-  ∀O:ordered_uniform_space.∀s:‡O.∀P:{[s]} squareO → Prop.∀OP:O squareO → Prop.Prop.
-apply(λO:ordered_uniform_space.λs:‡O.
-       λP:{[s]} squareO → Prop. λOP:O squareO → Prop.
-          ∀b:{[s]} squareO.(P b → OP b) ∧ (OP b → P b));
-qed.
-
-lemma unrestrict: ∀O:ordered_uniform_space.∀s:‡O.∀U,u.∀x:{[s]} squareO.
-  restriction_agreement ? s U u → U x → u x.
-intros 6; cases (H x); assumption;
-qed.
-
-lemma restrict: ∀O:ordered_uniform_space.∀s:‡O.∀U,u.∀x:{[s]} squareO.
-  restriction_agreement ? s U u → u x → U x.
-intros 6; cases (H x); assumption;
-qed.
-
-lemma invert_restriction_agreement: 
-  ∀O:ordered_uniform_space.∀s:‡O.
-   ∀U:{[s]} squareO → Prop.∀u:O squareO → Prop.
-    restriction_agreement ? s U u →
-    restriction_agreement ? s (\inv U) (\inv u).
-intros 6; cases b;
-generalize in match (H 〈h1,h〉); cases h; cases h1; simplify; 
-intro X; cases X; split; assumption; 
-qed. 
-
-lemma bs2_of_bss2: 
- ∀O:ordered_set.∀s:‡O.(bishop_set_of_ordered_set {[s]}) squareB → (bishop_set_of_ordered_set O) squareB ≝ 
-  λO:ordered_set.λs:‡O.λb:{[s]} squareO.〈\fst(\fst b),\fst(\snd b)〉.
-
-coercion bs2_of_bss2 nocomposites.
-
-
-lemma a2sa :
- ∀O:ordered_uniform_space.∀s:‡(ordered_set_OF_ordered_uniform_space O).
- ∀x:
-  bs_carr
-  (square_bishop_set
-   (bishop_set_of_ordered_set
-     (segment_ordered_set 
-       (ordered_set_OF_ordered_uniform_space O) s))).
- (\fst x) ≈ (\snd x) →
- (\fst (bs2_of_bss2 (ordered_set_OF_ordered_uniform_space O) s x))
- ≈
- (\snd (bs2_of_bss2 (ordered_set_OF_ordered_uniform_space O) s x)).
-intros 3; cases x (a b); clear x; simplify in match (\fst ?);
-simplify in match (\snd ?); intros 2 (K H); apply K; clear K;
-cases H; 
-[ left; change in H1:(? ? % ?) with (\fst a); 
-        change in H1:(? ? ? %) with (\fst b); 
-        change in a with (hos_carr (half_segment_ordered_set ? s));
-        change in b with (hos_carr (half_segment_ordered_set ? s));
-        apply rule H1;
-| right; change in H1:(? ? % ?) with (\fst b); 
-        change in H1:(? ? ? %) with (\fst a); 
-        change in a with (hos_carr (half_segment_ordered_set ? s));
-        change in b with (hos_carr (half_segment_ordered_set ? s));
-        apply rule H1;]
-qed.
-
-
-lemma segment_ordered_uniform_space: 
-  ∀O:ordered_uniform_space.∀s:‡O.ordered_uniform_space.
-intros (O s); apply mk_ordered_uniform_space;
-[1: apply (mk_ordered_uniform_space_ {[s]});
-    [1: alias symbol "and" = "constructive and".
-        letin f ≝ (λP:{[s]} squareO → Prop. ∃OP:O squareO → Prop.
-                    (us_unifbase O OP) ∧ restriction_agreement ?? P OP);
-        apply (mk_uniform_space (bishop_set_of_ordered_set {[s]}) f);
-        [1: intros (U H); intro x; simplify; 
-            cases H (w Hw); cases Hw (Gw Hwp); clear H Hw; intro Hm;
-            lapply (us_phi1 O w Gw x (a2sa ??? Hm)) as IH;
-            apply (restrict ? s ??? Hwp IH); 
-        |2: intros (U V HU HV); cases HU (u Hu); cases HV (v Hv); clear HU HV;
-            cases Hu (Gu HuU); cases Hv (Gv HvV); clear Hu Hv;
-            cases (us_phi2 O u v Gu Gv) (w HW); cases HW (Gw Hw); clear HW;
-            exists; [apply (λb:{[s]} squareB.w b)] split;
-            [1: unfold f; simplify; clearbody f;
-                exists; [apply w]; split; [assumption] intro b; simplify;
-                unfold segment_square_of_ordered_set_square;
-                cases b; intros; split; intros; assumption;
-            |2: intros 2 (x Hx); cases (Hw ? Hx); split;
-                [apply (restrict O s ??? HuU H)|apply (restrict O s ??? HvV H1);]]
-        |3: intros (U Hu); cases Hu (u HU); cases HU (Gu HuU); clear Hu HU;
-            cases (us_phi3 O u Gu) (w HW); cases HW (Gw Hwu); clear HW;
-            exists; [apply (λx:{[s]} squareB.w x)] split;
-            [1: exists;[apply w];split;[assumption] intros; simplify; intro;
-                unfold segment_square_of_ordered_set_square;
-                cases b; intros; split; intro; assumption;
-            |2: intros 2 (x Hx); apply (restrict O s ??? HuU); apply Hwu; 
-                cases Hx (m Hm); exists[apply (\fst m)] apply Hm;]
-        |4: intros (U HU x); cases HU (u Hu); cases Hu (Gu HuU); clear HU Hu;
-            cases (us_phi4 O u Gu x) (Hul Hur);
-            split; intros; 
-            [1: lapply (invert_restriction_agreement O s ?? HuU) as Ra;
-                apply (restrict O s ?? x Ra);
-                apply Hul; apply (unrestrict O s ??? HuU H);
-            |2: apply (restrict O s ??? HuU); apply Hur; 
-                apply (unrestrict O s ??? (invert_restriction_agreement O s ?? HuU) H);]]
-    |2: simplify; reflexivity;]
-|2: simplify; unfold convex; intros 3; cases s1; intros;
-    (* TODO: x2sx is for ≰, we need one for ≤ *) 
-    cases H (u HU); cases HU (Gu HuU); clear HU H;
-    lapply depth=0 (ous_convex_l ?? Gu 〈\fst h,\fst h1〉 ???????) as K3;
-    [2: intro; apply H2; apply (x2sx_ (os_l O) s h h1 H);
-    |3: apply 〈\fst (\fst y),\fst (\snd y)〉;
-    |4: intro; change in H with (\fst (\fst y) ≰ \fst h1); apply H3;
-        apply (x2sx_ (os_l O) s (\fst y) h1 H);
-    |5: change with (\fst h ≤ \fst (\fst y)); intro; apply H4;
-        apply (x2sx_ (os_l O) s h (\fst y) H);
-    |6: change with (\fst (\snd y) ≤ \fst h1); intro; apply H5;
-        apply (x2sx_ (os_l O) s (\snd y) h1 H);
-    |7: change with (\fst (\fst y) ≤ \fst (\snd y)); intro; apply H6;
-        apply (x2sx_ (os_l O) s (\fst y) (\snd y) H);
-    |8: apply (restrict O s U u y HuU K3);
-    |1: apply (unrestrict O s ?? 〈h,h1〉 HuU H1);]
-|3: simplify; unfold convex; intros 3; cases s1; intros;
-    cases H (u HU); cases HU (Gu HuU); clear HU H;
-    lapply depth=0 (ous_convex_r ?? Gu 〈\fst h,\fst h1〉 ???????) as K3;
-    [2: intro; apply H2; apply (x2sx_ (os_r O) s h h1 H);
-    |3: apply 〈\fst (\fst y),\fst (\snd y)〉;
-    |4: intro; apply H3;
-        apply (x2sx_ (os_r O) s (\fst y) h1 H);
-    |5: intro; apply H4;
-        apply (x2sx_ (os_r O) s h (\fst y) H);
-    |6: intro; apply H5;
-        apply (x2sx_ (os_r O) s (\snd y) h1 H);
-    |7: intro; apply H6;
-        apply (x2sx_ (os_r O) s (\fst y) (\snd y) H);
-    |8: apply (restrict O s U u y HuU K3);
-    |1: apply (unrestrict O s ?? 〈h,h1〉 HuU H1);]
-]  
-qed.
-
-interpretation "Ordered uniform space segment" 'segset a = 
- (segment_ordered_uniform_space _ a).
-
-(* Lemma 3.2 *)
-alias symbol "pi1" = "exT \fst".
-lemma restric_uniform_convergence:
- ∀O:ordered_uniform_space.∀s:‡O.
-  ∀x:{[s]}.
-   ∀a:sequence {[s]}.
-    (⌊n, \fst (a n)⌋ : sequence O) uniform_converges (\fst x) → 
-      a uniform_converges x.
-intros 7; cases H1; cases H2; clear H2 H1;
-cases (H ? H3) (m Hm); exists [apply m]; intros; 
-apply (restrict ? s ??? H4); apply (Hm ? H1);
-qed.
-
-definition order_continuity ≝
-  λC:ordered_uniform_space.∀a:sequence C.∀x:C.
-    (a ↑ x → a uniform_converges x) ∧ (a ↓ x → a uniform_converges x).
-
-lemma hint_boh1: ∀O. Type_OF_ordered_uniform_space O → hos_carr (os_l O).
-intros; assumption;
-qed.
-
-coercion hint_boh1 nocomposites. 
-
-lemma hint_boh2: ∀O:ordered_uniform_space. hos_carr (os_l O) → Type_OF_ordered_uniform_space O.
-intros; assumption;
-qed.
-
-coercion hint_boh2 nocomposites. 
-
diff --git a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
deleted file mode 100644
index deddf8804..000000000
--- a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
+++ /dev/null
@@ -1,171 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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 "ordered_uniform.ma".
-include "property_sigma.ma".
-
-lemma h_segment_upperbound:
-  ∀C:half_ordered_set.
-   ∀s:segment C.
-    ∀a:sequence (half_segment_ordered_set C s).
-      upper_bound ? ⌊n,\fst (a n)⌋ (seg_u C s). 
-intros 4; simplify; cases (a n); simplify; unfold in H;
-cases (wloss_prop C); rewrite < H1 in H; simplify; cases H; 
-assumption;
-qed.
-
-notation "'segment_upperbound'" non associative with precedence 90 for @{'segment_upperbound}.
-notation "'segment_lowerbound'" non associative with precedence 90 for @{'segment_lowerbound}.
-
-interpretation "segment_upperbound" 'segment_upperbound = (h_segment_upperbound (os_l _)).
-interpretation "segment_lowerbound" 'segment_lowerbound = (h_segment_upperbound (os_r _)).
-
-lemma h_segment_preserves_uparrow:
-  ∀C:half_ordered_set.∀s:segment C.∀a:sequence (half_segment_ordered_set C s).
-   ∀x,h. uparrow C ⌊n,\fst (a n)⌋ x → uparrow (half_segment_ordered_set C s) a ≪x,h≫.
-intros; cases H (Ha Hx); split;
-[ intro n; intro H; apply (Ha n); apply rule H;
-| cases Hx; split; 
-  [ intro n; intro H; apply (H1 n);apply rule H; 
-  | intros; cases (H2 (\fst y)); [2: apply rule H3;] 
-    exists [apply w] apply (x2sx_ ?? (a w) y H4);]]
-qed.
-
-notation "'segment_preserves_uparrow'" non associative with precedence 90 for @{'segment_preserves_uparrow}.
-notation "'segment_preserves_downarrow'" non associative with precedence 90 for @{'segment_preserves_downarrow}.
-
-interpretation "segment_preserves_uparrow" 'segment_preserves_uparrow = (h_segment_preserves_uparrow (os_l _)).
-interpretation "segment_preserves_downarrow" 'segment_preserves_downarrow = (h_segment_preserves_uparrow (os_r _)).
- 
-(* Fact 2.18 *)
-lemma segment_cauchy:
-  ∀C:ordered_uniform_space.∀s:‡C.∀a:sequence {[s]}.
-    a is_cauchy → ⌊n,\fst (a n)⌋ is_cauchy.
-intros 6; 
-alias symbol "pi1" (instance 3) = "pair pi1".
-alias symbol "pi2" = "pair pi2".
-apply (H (λx:{[s]} squareB.U 〈\fst (\fst x),\fst (\snd x)〉));
-(unfold segment_ordered_uniform_space; simplify);
-exists [apply U] split; [assumption;]
-intro; cases b; intros; simplify; split; intros; assumption;
-qed.       
-
-(* Definition 3.7 *)
-definition exhaustive ≝
-  λC:ordered_uniform_space.
-   ∀a,b:sequence C.
-     (a is_increasing → a is_upper_located → a is_cauchy) ∧
-     (b is_decreasing → b is_lower_located → b is_cauchy).
-
-lemma h_uparrow_to_in_segment:
-  ∀C:half_ordered_set.
-   ∀s:segment C.
-     ∀a:sequence C.
-      (∀i.a i ∈ s) →
-       ∀x:C. uparrow C a x → 
-         in_segment C s x.
-intros (C H a H1 x H2); unfold in H2; cases H2; clear H2;unfold in H3 H4; cases H4; clear H4; unfold in H2;
-cases (wloss_prop C) (W W); apply prove_in_segment; unfold; 
-[ apply (hle_transitive ??? x ? (H2 O)); lapply (H1 O) as K; unfold in K; rewrite <W in K;
-  cases K; unfold in H4 H6; apply H4;
-| intro; cases (H5 ? H4); clear H5 H4;lapply(H1 w) as K; unfold in K; rewrite<W in K;
-  cases K; unfold in H5 H4; apply H5; apply H6;    
-| apply (hle_transitive ??? x ?  (H2 O)); lapply (H1 0) as K; unfold in K; rewrite <W in K;
-  cases K; unfold in H4 H6; apply H6;
-| intro; cases (H5 ? H4); clear H5 H4;lapply(H1 w) as K; unfold in K; rewrite<W in K;
-  cases K; unfold in H5 H4; apply (H4 H6);]    
-qed.
-
-notation "'uparrow_to_in_segment'" non associative with precedence 90 for @{'uparrow_to_in_segment}.
-notation "'downarrow_to_in_segment'" non associative with precedence 90 for @{'downarrow_to_in_segment}.
-
-interpretation "uparrow_to_in_segment" 'uparrow_to_in_segment = (h_uparrow_to_in_segment (os_l _)).
-interpretation "downarrow_to_in_segment" 'downarrow_to_in_segment = (h_uparrow_to_in_segment (os_r _)).
- 
-(* Lemma 3.8 NON DUALIZZATO *)
-lemma restrict_uniform_convergence_uparrow:
-  ∀C:ordered_uniform_space.property_sigma C →
-    ∀s:segment (os_l C).exhaustive (segment_ordered_uniform_space C s) →
-     ∀a:sequence (segment_ordered_uniform_space C s).
-      ∀x:C. ⌊n,\fst (a n)⌋ ↑ x → 
-       in_segment (os_l C) s x ∧ ∀h:x ∈ s.a uniform_converges ≪x,h≫.
-intros; split;
-[1: apply (uparrow_to_in_segment s ⌊n,\fst (a \sub n)⌋ ? x H2); 
-    simplify; intros; cases (a i); assumption;
-|2: intros;
-    lapply (uparrow_upperlocated a ≪x,h≫) as Ha1;
-      [2: apply (segment_preserves_uparrow s); assumption;] 
-    lapply (segment_preserves_supremum s a ≪?,h≫ H2) as Ha2; 
-    cases Ha2; clear Ha2;
-    cases (H1 a a); lapply (H5 H3 Ha1) as HaC;
-    lapply (segment_cauchy C s ? HaC) as Ha;
-    lapply (sigma_cauchy ? H  ? x ? Ha); [left; assumption]
-    apply (restric_uniform_convergence C s ≪x,h≫ a Hletin)]
-qed.
-
-lemma hint_mah1:
-  ∀C. Type_OF_ordered_uniform_space1 C → hos_carr (os_r C).
-  intros; assumption; qed.
-  
-coercion hint_mah1 nocomposites.
-
-lemma hint_mah2:
-  ∀C. sequence (hos_carr (os_l C)) → sequence (hos_carr (os_r C)).
-  intros; assumption; qed.
-  
-coercion hint_mah2 nocomposites.
-
-lemma hint_mah3:
-  ∀C. Type_OF_ordered_uniform_space C → hos_carr (os_r C).
-  intros; assumption; qed.
-  
-coercion hint_mah3 nocomposites.
-    
-lemma hint_mah4:
-  ∀C. sequence (hos_carr (os_r C)) → sequence (hos_carr (os_l C)).
-  intros; assumption; qed.
-  
-coercion hint_mah4 nocomposites.
-
-lemma hint_mah5:
-  ∀C. segment (hos_carr (os_r C)) → segment (hos_carr (os_l C)).
-  intros; assumption; qed.
-  
-coercion hint_mah5 nocomposites.
-
-lemma hint_mah6:
-  ∀C. segment (hos_carr (os_l C)) → segment (hos_carr (os_r C)).
-  intros; assumption; qed.
-
-coercion hint_mah6 nocomposites.
-
-lemma restrict_uniform_convergence_downarrow:
-  ∀C:ordered_uniform_space.property_sigma C →
-    ∀s:segment (os_l C).exhaustive (segment_ordered_uniform_space C s) →
-     ∀a:sequence (segment_ordered_uniform_space C s).
-      ∀x:C. ⌊n,\fst (a n)⌋ ↓ x → 
-       in_segment (os_l C) s x ∧ ∀h:x ∈ s.a uniform_converges ≪x,h≫.
-intros; split;       
-[1: apply (downarrow_to_in_segment s ⌊n,\fst (a n)⌋ ? x); [2: apply H2]; 
-    simplify; intros; cases (a i); assumption;
-|2: intros;
-    lapply (downarrow_lowerlocated a ≪x,h≫) as Ha1;
-      [2: apply (segment_preserves_downarrow s a x h H2);] 
-    lapply (segment_preserves_infimum s a ≪?,h≫ H2) as Ha2; 
-    cases Ha2; clear Ha2;
-    cases (H1 a a); lapply (H6 H3 Ha1) as HaC;
-    lapply (segment_cauchy C s ? HaC) as Ha;
-    lapply (sigma_cauchy ? H  ? x ? Ha); [right; assumption]
-    apply (restric_uniform_convergence C s ≪x,h≫ a Hletin)]
-qed.
diff --git a/helm/software/matita/contribs/dama/dama/property_sigma.ma b/helm/software/matita/contribs/dama/dama/property_sigma.ma
deleted file mode 100644
index 74f03de4c..000000000
--- a/helm/software/matita/contribs/dama/dama/property_sigma.ma
+++ /dev/null
@@ -1,121 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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 "ordered_uniform.ma".
-include "russell_support.ma".
-
-(* Definition 3.5 *)
-alias num (instance 0) = "natural number".
-definition property_sigma ≝
-  λC:ordered_uniform_space.
-   ∀U.us_unifbase ? U → 
-     ∃V:sequence (C squareB → Prop).
-       (∀i.us_unifbase ? (V i)) ∧ 
-       ∀a:sequence C.∀x:C.(a ↑ x ∨ a ↓ x) → 
-         (∀n.∀i,j.n ≤ i → n ≤ j → V n 〈a i,a j〉) → U 〈a 0,x〉.
-      
-definition max ≝
-  λm,n.match leb n m with [true ⇒ m | false ⇒ n].
-  
-lemma le_max: ∀n,m.m ≤ max n m.
-intros; unfold max; apply leb_elim; simplify; intros; [assumption] apply le_n;
-qed.
-
-lemma max_le_l: ∀n,m,z.max n m ≤ z → n ≤ z.
-intros 3; unfold max; apply leb_elim; simplify; intros; [assumption]
-apply lt_to_le; apply (lt_to_le_to_lt ???? H1);
-apply not_le_to_lt; assumption;
-qed.
-
-lemma sym_max: ∀n,m.max n m = max m n.
-intros; apply (nat_elim2 ???? n m); simplify; intros;
-[1: elim n1; [reflexivity] rewrite < H in ⊢ (? ? ? (? %));
-    simplify; rewrite > H; reflexivity;
-|2: reflexivity
-|3: apply leb_elim; apply leb_elim; simplify;
-    [1: intros; apply le_to_le_to_eq; apply le_S_S;assumption;
-    |2,3: intros; reflexivity;
-    |4: intros; unfold max in H; 
-        rewrite > (?:leb n1 m1 = false) in H; [2:
-          apply lt_to_leb_false; apply not_le_to_lt; assumption;]
-        rewrite > (?:leb m1 n1 = false) in H; [2:
-          apply lt_to_leb_false; apply not_le_to_lt; assumption;]
-        apply eq_f; assumption;]]
-qed.
-
-lemma max_le_r: ∀n,m,z.max n m ≤ z → m ≤ z.
-intros; rewrite > sym_max in H; apply (max_le_l ??? H); 
-qed.
-  
-(* Lemma 3.6 *)   
-lemma sigma_cauchy:
-  ∀C:ordered_uniform_space.property_sigma C →
-    ∀a:sequence C.∀l:C.(a ↑ l ∨ a ↓ l) → a is_cauchy → a uniform_converges l.
-intros 8; cases (H ? H3) (w H5); cases H5 (H8 H9); clear H5;
-letin spec ≝ (λz,k:nat.∀i,j,l:nat.k ≤ i → k ≤ j → l ≤ z → w l 〈a i,a j〉);
-letin m ≝ (hide ? (let rec aux (i:nat) : nat ≝
-  match i with
-  [ O ⇒ match H2 (w i) ? with [ ex_introT k _ ⇒ k ]
-  | S i' ⇒ max (match H2 (w i) ? with [ ex_introT k _ ⇒ k ]) (S (aux i'))
-  ] in aux
-  : ∀z.∃k. spec z k)); unfold spec in aux ⊢ %;
-  [1,2:apply H8;
-  |3: intros 3; cases (H2 (w n) (H8 n)); simplify in ⊢ (? (? % ?) ?→?);
-      simplify in ⊢ (?→? (? % ?) ?→?);
-      intros; lapply (H5 i j) as H14;
-        [2: apply (max_le_l ??? H6);|3:apply (max_le_l ??? H7);]
-      cases (le_to_or_lt_eq ?? H10); [2: destruct H11; destruct H4; assumption]
-      cases (aux n1) in H6 H7 ⊢ %; simplify in ⊢ (? (? ? %) ?→? (? ? %) ?→?); intros;
-      apply H6; [3: apply le_S_S_to_le; assumption]
-      apply lt_to_le; apply (max_le_r w1); assumption;
-  |4: intros; clear H6; rewrite > H4 in H5; 
-      rewrite < (le_n_O_to_eq ? H11); apply H5; assumption;] 
-cut ((⌊x,(m x:nat)⌋ : sequence nat_ordered_set) is_strictly_increasing) as Hm; [2:
-  intro n; change with (S (m n) ≤ m (S n)); unfold m; 
-  whd in ⊢ (? ? %); apply (le_max ? (S (m n)));]
-cut ((⌊x,(m x:nat)⌋ : sequence nat_ordered_set) is_increasing) as Hm1; [2:
-  intro n; intro L; change in L with (m (S n) < m n);
-  lapply (Hm n) as L1; change in L1 with (m n < m (S n));
-  lapply (trans_lt ??? L L1) as L3; apply (not_le_Sn_n ? L3);] 
-clearbody m; unfold spec in m Hm Hm1; clear spec;
-cut (⌊x,a (m x)⌋ ↑ l ∨ ⌊x,a (m x)⌋ ↓ l) as H10; [2: 
- cases H1;
- [ left; apply (selection_uparrow ? Hm a l H4);
- | right; apply (selection_downarrow ? Hm a l H4);]] 
-lapply (H9 ?? H10) as H11; [
-  exists [apply (m 0:nat)] intros;
-  cases H1; cases H5; cases H7; cases (us_phi4 ?? H3 〈l,a i〉);
-  apply H15; change with (U 〈a i,l〉);
-    [apply (ous_convex_l C ? H3 ? H11 (H12 (m O)));
-    |apply (ous_convex_r C ? H3 ? H11 (H12 (m O)));]
-  [1:apply (H12 i);
-  |3: apply (le_reflexive l);
-  |4: apply (H12 i);
-  |2:change with (a (m O) ≤ a i);
-     apply (trans_increasing a H6 (\fst (m 0)) i); intro; apply (le_to_not_lt ?? H4 H16);
-  |5:apply (H12 i);
-  |7:apply (ge_reflexive (l : hos_carr (os_r C)));
-  |8:apply (H12 i);
-  |6:change with (a i ≤ a (m O));
-     apply (trans_decreasing ? H6 (\fst (m 0)) i); intro; apply (le_to_not_lt ?? H4 H16);]]  
-clear H10; intros (p q r); change with (w p 〈a (m q),a (m r)〉);
-generalize in match (refl_eq nat (m p)); 
-generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X (w1 H15); clear X; 
-intros (H16); simplify in H16:(? ? ? %); destruct H16;
-apply H15; [3: apply le_n]
-[1: lapply (trans_increasing ? Hm1 p q) as T; [apply not_lt_to_le; apply T;]
-    apply (le_to_not_lt p q H4);
-|2: lapply (trans_increasing ? Hm1 p r) as T; [apply not_lt_to_le; apply T;]
-    apply (le_to_not_lt p r H5);]
-qed.
diff --git a/helm/software/matita/contribs/dama/dama/russell_support.ma b/helm/software/matita/contribs/dama/dama/russell_support.ma
deleted file mode 100644
index deb5fc950..000000000
--- a/helm/software/matita/contribs/dama/dama/russell_support.ma
+++ /dev/null
@@ -1,27 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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 "nat/nat.ma".
-include "logic/cprop_connectives.ma".
-
-definition hide ≝ λT:Type.λx:T.x.
-
-notation < "\blacksquare" non associative with precedence 50 for @{'hide}.
-interpretation "hide" 'hide = (hide _ _).
-interpretation "hide2" 'hide = (hide _ _ _).
-
-definition inject ≝ λP.λa:nat.λp:P a. ex_introT ? P ? p.
-coercion cic:/matita/dama/russell_support/inject.con 0 1.
-definition eject ≝ λP.λc: ∃n:nat.P n. match c with [ ex_introT w _ ⇒ w].
-coercion cic:/matita/dama/russell_support/eject.con.
diff --git a/helm/software/matita/contribs/dama/dama/sandwich.ma b/helm/software/matita/contribs/dama/dama/sandwich.ma
deleted file mode 100644
index 68bb4453c..000000000
--- a/helm/software/matita/contribs/dama/dama/sandwich.ma
+++ /dev/null
@@ -1,48 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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 "ordered_uniform.ma".
-
-lemma le_w_plus: ∀n,m,o.n+m≤o → m ≤ o.
-intro; elim n; simplify; [assumption]
-lapply (le_S ?? H1); apply H; apply le_S_S_to_le; assumption;
-qed.
-
-alias symbol "leq" = "Ordered set less or equal than".
-alias symbol "and" = "logical and".
-theorem sandwich: 
-  ∀O:ordered_uniform_space.∀l:O.∀a,b,x:sequence O.
-   (∀i:nat.a i ≤ x i ∧ x i ≤ b i) →
-    a uniform_converges l → 
-     b uniform_converges l → 
-      x uniform_converges l.
-intros 10; 
-cases (us_phi3 ? ? H3) (V GV); cases GV (Gv HV); clear GV;
-cases (us_phi3 ? ? Gv) (W GW); cases GW (Gw HW); clear GW;
-cases (H1 ? Gw) (ma Hma); cases (H2 ? Gw) (mb Hmb); clear H1 H2;
-exists [apply (ma + mb)] intros; apply (HV 〈l,(x i)〉); 
-unfold; simplify; exists [apply (a i)] split;
-[2: apply (ous_convex_l ?? Gv 〈a i,b i〉); cases (H i) (Lax Lxb); clear H;
-    [1: apply HW; exists [apply l]simplify; split; 
-        [1: cases (us_phi4 ?? Gw 〈(a i),l〉); apply H2; clear H2 H;
-            apply (Hma i); rewrite > sym_plus in H1; apply (le_w_plus mb); assumption;
-        |2: apply Hmb; apply (le_w_plus ma); assumption] 
-    |2,3: simplify; apply (le_transitive (a i) ?? Lax Lxb);
-    |4: apply (le_reflexive);
-    |5,6: assumption;]
-|1: apply HW; exists[apply l] simplify; split;
-    [1: apply (us_phi1 ?? Gw); unfold; apply eq_reflexive;
-    |2: apply Hma;  rewrite > sym_plus in H1; apply (le_w_plus mb); assumption;]]
-qed. 
- 
diff --git a/helm/software/matita/contribs/dama/dama/sequence.ma b/helm/software/matita/contribs/dama/dama/sequence.ma
deleted file mode 100644
index 948d14f67..000000000
--- a/helm/software/matita/contribs/dama/dama/sequence.ma
+++ /dev/null
@@ -1,38 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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 "nat/nat.ma".
-
-inductive sequence (O:Type) : Type ≝  
- | mk_seq : (nat → O) → sequence O.
-
-definition fun_of_seq: ∀O:Type.sequence O → nat → O ≝ 
-  λO.λx:sequence O.match x with [ mk_seq f ⇒ f ].
-
-coercion cic:/matita/dama/sequence/fun_of_seq.con 1.
-
-notation < "hvbox((\lfloor term 19 p \rfloor) \sub ident i)" with precedence 90
-for @{ 'sequence (\lambda ${ident i} : $t . $p)}.
-
-notation > "hvbox((\lfloor term 19 p \rfloor) \sub ident i)" with precedence 90
-for @{ 'sequence (\lambda ${ident i} . $p)}.
-
-notation > "hvbox(\lfloor ident i, term 19 p \rfloor)" with precedence 90
-for @{ 'sequence (\lambda ${ident i} . $p)}.
-  
-notation "a \sub i" left associative with precedence 90 
-  for @{ 'sequence_appl $a $i }.
-
-interpretation "sequence" 'sequence \eta.x = (mk_seq _ x).
-interpretation "sequence element" 'sequence_appl s i = (fun_of_seq _ s i).
diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
deleted file mode 100644
index 0de61b292..000000000
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ /dev/null
@@ -1,442 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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 "datatypes/constructors.ma".
-include "nat/plus.ma".
-include "nat_ordered_set.ma".
-include "sequence.ma".
-
-(* Definition 2.4 *)
-definition upper_bound ≝ 
-  λO:half_ordered_set.λa:sequence O.λu:O.∀n:nat.a n ≤≤ u.
-
-definition supremum ≝
-  λO:half_ordered_set.λs:sequence O.λx.
-    upper_bound ? s x ∧ (∀y:O.x ≰≰ y → ∃n.s n ≰≰ y).
-
-definition increasing ≝ 
-  λO:half_ordered_set.λa:sequence O.∀n:nat.a n ≤≤ a (S n).
-
-notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 45 
-  for @{'upper_bound $s $x}.
-notation < "x \nbsp 'is_lower_bound' \nbsp s" non associative with precedence 45 
-  for @{'lower_bound $s $x}.
-notation < "s \nbsp 'is_increasing'" non associative with precedence 45 
-  for @{'increasing $s}.
-notation < "s \nbsp 'is_decreasing'" non associative with precedence 45 
-  for @{'decreasing $s}.
-notation < "x \nbsp 'is_supremum' \nbsp s" non associative with precedence 45 
-  for @{'supremum $s $x}.
-notation < "x \nbsp 'is_infimum' \nbsp s" non associative with precedence 45 
-  for @{'infimum $s $x}.
-notation > "x 'is_upper_bound' s" non associative with precedence 45 
-  for @{'upper_bound $s $x}.
-notation > "x 'is_lower_bound' s" non associative with precedence 45 
-  for @{'lower_bound $s $x}.
-notation > "s 'is_increasing'"    non associative with precedence 45 
-  for @{'increasing $s}.
-notation > "s 'is_decreasing'"    non associative with precedence 45 
-  for @{'decreasing $s}.
-notation > "x 'is_supremum' s"  non associative with precedence 45 
-  for @{'supremum $s $x}.
-notation > "x 'is_infimum' s"  non associative with precedence 45 
-  for @{'infimum $s $x}.
-
-interpretation "Ordered set upper bound" 'upper_bound s x = (upper_bound (os_l _) s x).
-interpretation "Ordered set lower bound" 'lower_bound s x = (upper_bound (os_r _) s x).
-
-interpretation "Ordered set increasing"  'increasing s = (increasing (os_l _) s).
-interpretation "Ordered set decreasing"  'decreasing s = (increasing (os_r _) s).
-
-interpretation "Ordered set strong sup"  'supremum s x = (supremum (os_l _) s x).
-interpretation "Ordered set strong inf"  'infimum s x = (supremum (os_r _) s x).
-  
-(* Fact 2.5 *)
-lemma h_supremum_is_upper_bound: 
-  ∀C:half_ordered_set.∀a:sequence C.∀u:C.
-   supremum ? a u → ∀v.upper_bound ? a v → u ≤≤ v.
-intros 7 (C s u Hu v Hv H); cases Hu (_ H1); clear Hu;
-cases (H1 ? H) (w Hw); apply Hv; [apply w] assumption;
-qed.
-
-notation "'supremum_is_upper_bound'" non associative with precedence 90 for @{'supremum_is_upper_bound}.
-notation "'infimum_is_lower_bound'" non associative with precedence 90 for @{'infimum_is_lower_bound}.
-
-interpretation "supremum_is_upper_bound" 'supremum_is_upper_bound = (h_supremum_is_upper_bound (os_l _)).
-interpretation "infimum_is_lower_bound" 'infimum_is_lower_bound = (h_supremum_is_upper_bound (os_r _)).
-
-(* Lemma 2.6 *)
-definition strictly_increasing ≝ 
-  λC:half_ordered_set.λa:sequence C.∀n:nat.a (S n) ≰≰ a n.
-
-notation < "s \nbsp 'is_strictly_increasing'" non associative with precedence 45 
-  for @{'strictly_increasing $s}.
-notation > "s 'is_strictly_increasing'" non associative with precedence 45 
-  for @{'strictly_increasing $s}.
-interpretation "Ordered set strict increasing"  'strictly_increasing s    = 
-  (strictly_increasing (os_l _) s).
-  
-notation < "s \nbsp 'is_strictly_decreasing'" non associative with precedence 45 
-  for @{'strictly_decreasing $s}.
-notation > "s 'is_strictly_decreasing'" non associative with precedence 45 
-  for @{'strictly_decreasing $s}.
-interpretation "Ordered set strict decreasing"  'strictly_decreasing s    = 
-  (strictly_increasing (os_r _) s).
-
-definition uparrow ≝
-  λC:half_ordered_set.λs:sequence C.λu:C.
-   increasing ? s ∧ supremum ? s u.
-
-interpretation "Ordered set uparrow" 'funion s u = (uparrow (os_l _) s u).
-interpretation "Ordered set downarrow" 'fintersects s u = (uparrow (os_r _) s u).
-
-lemma h_trans_increasing: 
-  ∀C:half_ordered_set.∀a:sequence C.increasing ? a → 
-   ∀n,m:nat_ordered_set. n ≤ m → a n ≤≤ a m.
-intros 5 (C a Hs n m); elim m; [
-  rewrite > (le_n_O_to_eq n (not_lt_to_le O n H));
-  intro X; cases (hos_coreflexive ? (a n) X);]
-cases (le_to_or_lt_eq ?? (not_lt_to_le (S n1) n H1)); clear H1;
-[2: rewrite > H2; intro; cases (hos_coreflexive ? (a (S n1)) H1);
-|1: apply (hle_transitive ???? (H ?) (Hs ?));
-    intro; whd in H1; apply (not_le_Sn_n n); apply (transitive_le ??? H2 H1);]
-qed.
-
-notation "'trans_increasing'" non associative with precedence 90 for @{'trans_increasing}.
-notation "'trans_decreasing'" non associative with precedence 90 for @{'trans_decreasing}.
-
-interpretation "trans_increasing" 'trans_increasing = (h_trans_increasing (os_l _)).
-interpretation "trans_decreasing" 'trans_decreasing = (h_trans_increasing (os_r _)).
-
-lemma hint_nat :
- Type_of_ordered_set nat_ordered_set →
-   hos_carr (os_l (nat_ordered_set)).
-intros; assumption;
-qed.
-
-coercion hint_nat nocomposites.
-
-lemma h_trans_increasing_exc: 
-  ∀C:half_ordered_set.∀a:sequence C.increasing ? a → 
-   ∀n,m:nat_ordered_set. m ≰≰ n → a n ≤≤ a m.
-intros 5 (C a Hs n m); elim m; [cases (not_le_Sn_O n H);]
-intro; apply H; 
-[1: change in n1 with (hos_carr (os_l nat_ordered_set)); 
-    change with (n<n1);
-    cases (le_to_or_lt_eq ?? H1); [apply le_S_S_to_le;assumption]
-    cases (Hs n); rewrite < H3 in H2; assumption;    
-|2: cases (hos_cotransitive ? (a n) (a (S n1)) (a n1) H2); [assumption]
-    cases (Hs n1); assumption;]
-qed.
-
-notation "'trans_increasing_exc'" non associative with precedence 90 for @{'trans_increasing_exc}.
-notation "'trans_decreasing_exc'" non associative with precedence 90 for @{'trans_decreasing_exc}.
-
-interpretation "trans_increasing_exc" 'trans_increasing_exc = (h_trans_increasing_exc (os_l _)).
-interpretation "trans_decreasing_exc" 'trans_decreasing_exc = (h_trans_increasing_exc (os_r _)).
-
-alias symbol "exists" = "CProp exists".
-lemma nat_strictly_increasing_reaches: 
-  ∀m:sequence nat_ordered_set.
-   m is_strictly_increasing → ∀w.∃t.m t ≰ w.
-intros; elim w;
-[1: cases (nat_discriminable O (m O)); [2: cases (not_le_Sn_n O (ltn_to_ltO ?? H1))]
-    cases H1; [exists [apply O] apply H2;]
-    exists [apply (S O)] lapply (H O) as H3; rewrite < H2 in H3; assumption
-|2: cases H1 (p Hp); cases (nat_discriminable (S n) (m p)); 
-    [1: cases H2; clear H2;
-        [1: exists [apply p]; assumption;
-        |2: exists [apply (S p)]; rewrite > H3; apply H;]
-    |2: cases (?:False); change in Hp with (n<m p);
-        apply (not_le_Sn_n (m p));
-        apply (transitive_le ??? H2 Hp);]]
-qed.
-     
-lemma h_selection_uparrow: 
-  ∀C:half_ordered_set.∀m:sequence nat_ordered_set.
-   m is_strictly_increasing →
-    ∀a:sequence C.∀u.uparrow ? a u → uparrow ? ⌊x,a (m x)⌋ u.
-intros (C m Hm a u Ha); cases Ha (Ia Su); cases Su (Uu Hu); repeat split; 
-[1: intro n; simplify; apply (h_trans_increasing_exc ? a Ia); apply (Hm n);
-|2: intro n; simplify; apply Uu;
-|3: intros (y Hy); simplify; cases (Hu ? Hy);
-    cases (nat_strictly_increasing_reaches ? Hm w); 
-    exists [apply w1]; cases (hos_cotransitive ? (a w) y (a (m w1)) H); [2:assumption]  
-    cases (h_trans_increasing_exc ?? Ia w (m w1) H1); assumption;]
-qed.     
-
-notation "'selection_uparrow'" non associative with precedence 90 for @{'selection_uparrow}.
-notation "'selection_downarrow'" non associative with precedence 90 for @{'selection_downarrow}.
-
-interpretation "selection_uparrow" 'selection_uparrow = (h_selection_uparrow (os_l _)).
-interpretation "selection_downarrow" 'selection_downarrow = (h_selection_uparrow (os_r _)).
-
-(* Definition 2.7 *)
-definition order_converge ≝
-  λO:ordered_set.λa:sequence O.λx:O.
-   exT23 (sequence O) (λl.l ↑ x) (λu.u ↓ x)
-     (λl,u:sequence O.∀i:nat. (l i) is_infimum ⌊w,a (w+i)⌋ ∧ 
-                   (u i) is_supremum ⌊w,a (w+i)⌋).
-    
-notation < "a \nbsp (\cir \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 45 
-  for @{'order_converge $a $x}.
-notation > "a 'order_converges' x" non associative with precedence 45 
-  for @{'order_converge $a $x}.
-interpretation "Order convergence" 'order_converge s u = (order_converge _ s u).   
-    
-(* Definition 2.8 *)
-record segment (O : Type) : Type ≝ {
-   seg_l_ : O;
-   seg_u_ : O
-}.
-
-notation > "𝕦_term 90 s" non associative with precedence 90 for @{'upp $s}.
-notation "𝕦 \sub term 90 s" non associative with precedence 90 for @{'upp $s}. 
-notation > "𝕝_term 90 s" non associative with precedence 90 for @{'low $s}.
-notation "𝕝 \sub term 90 s" non associative with precedence 90 for @{'low $s}. 
- 
-definition seg_u ≝
- λO:half_ordered_set.λs:segment O.
-   wloss O ?? (λl,u.l) (seg_u_ ? s) (seg_l_ ? s).
-definition seg_l ≝
- λO:half_ordered_set.λs:segment O.
-   wloss O ?? (λl,u.l) (seg_l_ ? s) (seg_u_ ? s). 
- 
-interpretation "uppper" 'upp s = (seg_u (os_l _) s).
-interpretation "lower" 'low s = (seg_l (os_l _) s).
-interpretation "uppper dual" 'upp s = (seg_l (os_r _) s).
-interpretation "lower dual" 'low s = (seg_u (os_r _) s).
- 
-definition in_segment ≝ 
-  λO:half_ordered_set.λs:segment O.λx:O.
-    wloss O ?? (λp1,p2.p1 ∧ p2) (seg_l ? s ≤≤ x) (x ≤≤ seg_u ? s).
-
-notation "‡O" non associative with precedence 90 for @{'segment $O}.
-interpretation "Ordered set sergment" 'segment x = (segment x).
-
-interpretation "Ordered set sergment in" 'mem x s = (in_segment _ s x).
-
-definition segment_ordered_set_carr ≝
-  λO:half_ordered_set.λs:‡O.∃x.x ∈ s.
-definition segment_ordered_set_exc ≝ 
-  λO:half_ordered_set.λs:‡O.
-   λx,y:segment_ordered_set_carr O s.hos_excess_ O (\fst x) (\fst y).
-lemma segment_ordered_set_corefl:
- ∀O,s. coreflexive ? (wloss O ?? (segment_ordered_set_exc O s)).
-intros 3; cases x; cases (wloss_prop O);
-generalize in match (hos_coreflexive O w);
-rewrite < (H1 ?? (segment_ordered_set_exc O s));
-rewrite < (H1 ?? (hos_excess_ O)); intros; assumption;
-qed.
-lemma segment_ordered_set_cotrans : 
-  ∀O,s. cotransitive ? (wloss O ?? (segment_ordered_set_exc O s)).
-intros 5 (O s x y z); cases x; cases y ; cases z; clear x y z;
-generalize in match (hos_cotransitive O w w1 w2);
-cases (wloss_prop O); 
-do 3 rewrite < (H3 ?? (segment_ordered_set_exc O s));
-do 3 rewrite < (H3 ?? (hos_excess_ O)); intros; apply H4; assumption;
-qed.  
-  
-lemma half_segment_ordered_set: 
-  ∀O:half_ordered_set.∀s:segment O.half_ordered_set.
-intros (O a); constructor 1;
-[ apply (segment_ordered_set_carr O a);
-| apply (wloss O);
-| apply (wloss_prop O);
-| apply (segment_ordered_set_exc O a);
-| apply (segment_ordered_set_corefl O a);
-| apply (segment_ordered_set_cotrans ??);
-]
-qed.
-
-lemma segment_ordered_set: 
-  ∀O:ordered_set.∀s:‡O.ordered_set.
-intros (O s); 
-apply half2full; apply (half_segment_ordered_set (os_l O) s); 
-qed.
-
-notation "{[ term 19 s ]}" non associative with precedence 90 for @{'segset $s}.
-interpretation "Ordered set segment" 'segset s = (segment_ordered_set _ s). 
-
-(* test :
- ∀O:ordered_set.∀s: segment (os_l O).∀x:O.
-   in_segment (os_l O) s x
-   =
-   in_segment (os_r O) s x.
-intros; try reflexivity;
-*)
-
-lemma prove_in_segment: 
- ∀O:half_ordered_set.∀s:segment O.∀x:O.
-   (seg_l O s) ≤≤ x → x ≤≤ (seg_u O s) → x ∈ s.
-intros; unfold; cases (wloss_prop O); rewrite < H2;
-split; assumption;
-qed.
-
-lemma cases_in_segment: 
-  ∀C:half_ordered_set.∀s:segment C.∀x. x ∈ s → (seg_l C s) ≤≤ x ∧ x ≤≤ (seg_u C s).
-intros; unfold in H; cases (wloss_prop C) (W W); rewrite<W in H; [cases H; split;assumption]
-cases H; split; assumption;
-qed. 
-
-definition hint_sequence: 
-  ∀C:ordered_set.
-    sequence (hos_carr (os_l C)) → sequence (Type_of_ordered_set C).
-intros;assumption;
-qed.
-
-definition hint_sequence1: 
-  ∀C:ordered_set.
-    sequence (hos_carr (os_r C)) → sequence (Type_of_ordered_set_dual C).
-intros;assumption;
-qed.
-
-definition hint_sequence2: 
-  ∀C:ordered_set.
-    sequence (Type_of_ordered_set C) → sequence (hos_carr (os_l C)).
-intros;assumption;
-qed.
-
-definition hint_sequence3: 
-  ∀C:ordered_set.
-    sequence (Type_of_ordered_set_dual C) → sequence (hos_carr (os_r C)).
-intros;assumption;
-qed.
-
-coercion hint_sequence nocomposites.
-coercion hint_sequence1 nocomposites.
-coercion hint_sequence2 nocomposites.
-coercion hint_sequence3 nocomposites.
-
-(* Lemma 2.9 - non easily dualizable *)
-
-lemma x2sx_:
-  ∀O:half_ordered_set.
-   ∀s:segment O.∀x,y:half_segment_ordered_set ? s.
-    \fst x ≰≰ \fst y → x ≰≰ y.
-intros 4; cases x; cases y; clear x y; simplify; unfold hos_excess;
-whd in ⊢ (?→? (% ? ?)? ? ? ? ?); simplify in ⊢ (?→%);
-cases (wloss_prop O) (E E); do 2 rewrite < E; intros; assumption;
-qed.
-
-lemma sx2x_:
-  ∀O:half_ordered_set.
-   ∀s:segment O.∀x,y:half_segment_ordered_set ? s.
-    x ≰≰ y → \fst x ≰≰ \fst y.
-intros 4; cases x; cases y; clear x y; simplify; unfold hos_excess;
-whd in ⊢ (? (% ? ?) ?? ? ? ? → ?); simplify in ⊢ (% → ?);
-cases (wloss_prop O) (E E); do 2 rewrite < E; intros; assumption;
-qed.
-
-lemma l2sl_:
-  ∀C,s.∀x,y:half_segment_ordered_set C s. \fst x ≤≤ \fst y → x ≤≤ y.
-intros; intro; apply H; apply sx2x_; apply H1;
-qed.
-
-
-lemma sl2l_:
-  ∀C,s.∀x,y:half_segment_ordered_set C s. x ≤≤ y → \fst x ≤≤ \fst y.
-intros; intro; apply H; apply x2sx_; apply H1;
-qed.
-
-coercion x2sx_ nocomposites.
-coercion sx2x_ nocomposites.
-coercion l2sl_ nocomposites.
-coercion sl2l_ nocomposites.
-
-lemma h_segment_preserves_supremum:
-  ∀O:half_ordered_set.∀s:segment O.
-   ∀a:sequence (half_segment_ordered_set ? s).
-    ∀x:half_segment_ordered_set ? s. 
-      increasing ? ⌊n,\fst (a n)⌋ ∧ 
-      supremum ? ⌊n,\fst (a n)⌋ (\fst x) → uparrow ? a x.
-intros; split; cases H; clear H; 
-[1: intro n; lapply (H1 n) as K; clear H1 H2;
-    intro; apply K; clear K; apply rule H; 
-|2: cases H2; split; clear H2;
-    [1: intro n; lapply (H n) as K; intro W; apply K;
-        apply rule W;
-    |2: clear H1 H; intros (y0 Hy0); cases (H3 (\fst y0));[exists[apply w]]
-        [1: change in H with (\fst (a w) ≰≰ \fst y0); apply rule H;
-        |2: apply rule Hy0;]]]
-qed.
-
-notation "'segment_preserves_supremum'" non associative with precedence 90 for @{'segment_preserves_supremum}.
-notation "'segment_preserves_infimum'" non associative with precedence 90 for @{'segment_preserves_infimum}.
-
-interpretation "segment_preserves_supremum" 'segment_preserves_supremum = (h_segment_preserves_supremum (os_l _)).
-interpretation "segment_preserves_infimum" 'segment_preserves_infimum = (h_segment_preserves_supremum (os_r _)).
-
-(*
-test segment_preserves_infimum2:
-  ∀O:ordered_set.∀s:‡O.∀a:sequence {[s]}.∀x:{[s]}. 
-    ⌊n,\fst (a n)⌋ is_decreasing ∧ 
-    (\fst x) is_infimum ⌊n,\fst (a n)⌋ → a ↓ x.
-intros; apply (segment_preserves_infimum s a x H);
-qed.
-*)
-       
-(* Definition 2.10 *)
-
-alias symbol "pi2" = "pair pi2".
-alias symbol "pi1" = "pair pi1".
-(*
-definition square_segment ≝ 
-  λO:half_ordered_set.λs:segment O.λx: square_half_ordered_set O.
-    in_segment ? s (\fst x) ∧ in_segment ? s (\snd x).
-*) 
-definition convex ≝
-  λO:half_ordered_set.λU:square_half_ordered_set O → Prop.
-    ∀s.U s → le O (\fst s) (\snd s) → 
-     ∀y. 
-       le O (\fst y) (\snd s) → 
-       le O (\fst s) (\fst y) →
-       le O (\snd y) (\snd s) →
-       le O (\fst y) (\snd y) →
-       U y.
-  
-(* Definition 2.11 *)  
-definition upper_located ≝
-  λO:half_ordered_set.λa:sequence O.∀x,y:O. y ≰≰ x → 
-    (∃i:nat.a i ≰≰ x) ∨ (∃b:O.y ≰≰ b ∧ ∀i:nat.a i ≤≤ b).
-
-notation < "s \nbsp 'is_upper_located'" non associative with precedence 45 
-  for @{'upper_located $s}.
-notation > "s 'is_upper_located'" non associative with precedence 45 
-  for @{'upper_located $s}.
-interpretation "Ordered set upper locatedness" 'upper_located s = 
-  (upper_located (os_l _) s).
-
-notation < "s \nbsp 'is_lower_located'" non associative with precedence 45 
-  for @{'lower_located $s}.
-notation > "s 'is_lower_located'" non associative with precedence 45
-  for @{'lower_located $s}.
-interpretation "Ordered set lower locatedness" 'lower_located s = 
-  (upper_located (os_r _) s).
-      
-(* Lemma 2.12 *)    
-lemma h_uparrow_upperlocated:
-  ∀C:half_ordered_set.∀a:sequence C.∀u:C.uparrow ? a u → upper_located ? a.
-intros (C a u H); cases H (H2 H3); clear H; intros 3 (x y Hxy);
-cases H3 (H4 H5); clear H3; cases (hos_cotransitive C y x u Hxy) (W W);
-[2: cases (H5 x W) (w Hw); left; exists [apply w] assumption;
-|1: right; exists [apply u]; split; [apply W|apply H4]]
-qed.
-
-notation "'uparrow_upperlocated'" non associative with precedence 90 for @{'uparrow_upperlocated}.
-notation "'downarrow_lowerlocated'" non associative with precedence 90 for @{'downarrow_lowerlocated}.
-
-interpretation "uparrow_upperlocated" 'uparrow_upperlocated = (h_uparrow_upperlocated (os_l _)).
-interpretation "downarrow_lowerlocated" 'downarrow_lowerlocated = (h_uparrow_upperlocated (os_r _)).
diff --git a/helm/software/matita/contribs/dama/dama/uniform.ma b/helm/software/matita/contribs/dama/dama/uniform.ma
deleted file mode 100644
index 759037124..000000000
--- a/helm/software/matita/contribs/dama/dama/uniform.ma
+++ /dev/null
@@ -1,92 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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 "supremum.ma".
-
-(* Definition 2.13 *)
-alias symbol "pair" = "Pair construction".
-alias symbol "exists" = "exists".
-alias symbol "and" = "logical and".
-definition compose_bs_relations ≝
-  λC:bishop_set.λU,V:C squareB → Prop.
-   λx:C squareB.∃y:C. U 〈\fst x,y〉 ∧ V 〈y,\snd x〉.
-   
-definition compose_os_relations ≝
-  λC:ordered_set.λU,V:C squareB → Prop.
-   λx:C squareB.∃y:C. U 〈\fst x,y〉 ∧ V 〈y,\snd x〉.
-   
-interpretation "bishop set relations composition" 'compose a b = (compose_bs_relations _ a b).
-interpretation "ordered set relations composition" 'compose a b = (compose_os_relations _ a b).
-
-definition invert_bs_relation ≝
-  λC:bishop_set.λU:C squareB → Prop.
-    λx:C squareB. U 〈\snd x,\fst x〉.
-      
-notation > "\inv" with precedence 60 for @{ 'invert_symbol  }.
-interpretation "relation invertion" 'invert a = (invert_bs_relation _ a).
-interpretation "relation invertion" 'invert_symbol = (invert_bs_relation _).
-interpretation "relation invertion" 'invert_appl a x = (invert_bs_relation _ a x).
-
-alias symbol "exists" = "CProp exists".
-alias symbol "compose" = "bishop set relations composition".
-alias symbol "and" (instance 21) = "constructive and".
-alias symbol "and" (instance 16) = "constructive and".
-alias symbol "and" (instance 9) = "constructive and".
-record uniform_space : Type ≝ {
-  us_carr:> bishop_set;
-  us_unifbase: (us_carr squareB → Prop) → CProp;
-  us_phi1: ∀U:us_carr squareB → Prop. us_unifbase U → 
-    (λx:us_carr squareB.\fst x ≈ \snd x) ⊆ U;
-  us_phi2: ∀U,V:us_carr squareB → Prop. us_unifbase U → us_unifbase V →
-    ∃W:us_carr squareB → Prop.us_unifbase W ∧ (W ⊆ (λx.U x ∧ V x));
-  us_phi3: ∀U:us_carr squareB → Prop. us_unifbase U → 
-    ∃W:us_carr squareB → Prop.us_unifbase W ∧ (W ∘ W) ⊆ U;
-  us_phi4: ∀U:us_carr squareB → Prop. us_unifbase U → ∀x.(U x → (\inv U) x) ∧ ((\inv U) x → U x)
-}.
-
-(* Definition 2.14 *)  
-alias symbol "leq" = "natural 'less or equal to'".
-definition cauchy ≝
-  λC:uniform_space.λa:sequence C.∀U.us_unifbase C U → 
-   ∃n. ∀i,j. n ≤ i → n ≤ j → U 〈a i,a j〉.
-   
-notation < "a \nbsp 'is_cauchy'" non associative with precedence 45 
-  for @{'cauchy $a}.
-notation > "a 'is_cauchy'" non associative with precedence 45 
-  for @{'cauchy $a}.
-interpretation "Cauchy sequence" 'cauchy s = (cauchy _ s).  
-   
-(* Definition 2.15 *)  
-definition uniform_converge ≝
-  λC:uniform_space.λa:sequence C.λu:C.
-    ∀U.us_unifbase C U →  ∃n. ∀i. n ≤ i → U 〈u,a i〉.
-    
-notation < "a \nbsp (\u \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 45 
-  for @{'uniform_converge $a $x}.
-notation > "a 'uniform_converges' x" non associative with precedence 45 
-  for @{'uniform_converge $a $x}.
-interpretation "Uniform convergence" 'uniform_converge s u =
- (uniform_converge _ s u).
- 
-(* Lemma 2.16 *)
-lemma uniform_converge_is_cauchy : 
-  ∀C:uniform_space.∀a:sequence C.∀x:C.
-   a uniform_converges x → a is_cauchy. 
-intros (C a x Ha); intros 2 (u Hu);
-cases (us_phi3 ?? Hu) (v Hv0); cases Hv0 (Hv H); clear Hv0;
-cases (Ha ? Hv) (n Hn); exists [apply n]; intros;
-apply H; unfold; exists [apply x]; split [2: apply (Hn ? H2)]
-cases (us_phi4 ?? Hv 〈a i,x〉) (P1 P2); apply P2;
-apply (Hn ? H1);
-qed.