X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Flebesgue.ma;h=1536476b09c0a91e22e9c3f87570dc58a6b54f7f;hb=5322d66340d43e85b85e15dddcddeff3ae3a3552;hp=5957235ccc183793c5c1e1a209c9f4ca1ecc4de5;hpb=f20f1ac4aea15d81599bd2283c5440fce8d4cf6a;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma
index 5957235cc..1536476b0 100644
--- a/helm/software/matita/contribs/dama/dama/lebesgue.ma
+++ b/helm/software/matita/contribs/dama/dama/lebesgue.ma
@@ -59,14 +59,6 @@ cases (wloss_prop (os_l C))(W W); unfold os_r; unfold dual_hos; simplify;rewrite
   rewrite <W in H1; simplify in H1; apply (H1 Hw);]
 qed. 
 
-alias symbol "upp" = "uppper".
-alias symbol "leq" = "Ordered set less or equal than".
-lemma cases_in_segment: 
-  ∀C:half_ordered_set.∀s:segment C.∀x. x ∈ s → seg_l C s (λl.l ≤≤ x) ∧ seg_u C s (λu.x ≤≤ u).
-intros; unfold in H; cases (wloss_prop C) (W W); rewrite<W in H; [cases H; split;assumption]
-cases H; split; assumption;
-qed. 
-
 lemma trans_under_upp:
  ∀O:ordered_set.∀s:‡O.∀x,y:O.
   x ≤ y → 𝕦_s (λu.y ≤ u) → 𝕦_s (λu.x ≤ u).