duality is a joke

[helm.git] / helm / software / matita / contribs / dama / dama / bishop_set.ma

diff --git a/helm/software/matita/contribs/dama/dama/bishop_set.ma b/helm/software/matita/contribs/dama/dama/bishop_set.ma
index 3522a3bb206d93615a489b7317244b846aea45bd..d69bb2732b3f1a4a023aa21bdd54fc4635c3b7b7 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/bishop_set.ma
+++ b/helm/software/matita/contribs/dama/dama/bishop_set.ma
@@ -67,30 +67,6 @@ 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 lt ≝ λE:half_ordered_set.λa,b:E. a ≤ b ∧ a # b.
-
-interpretation "ordered sets less than" 'lt a b = (lt _ a b).
-
-lemma lt_coreflexive: ∀E.coreflexive ? (lt E).
-intros 2 (E x); intro H; cases H (_ ABS);
-apply (bs_coreflexive ? x ABS);
-qed.
-
-lemma lt_transitive: ∀E.transitive ? (lt E).
-intros (E); unfold; intros (x y z H1 H2); cases H1 (Lxy Axy); cases H2 (Lyz Ayz);
-split; [apply (le_transitive E ??? Lxy Lyz)] clear H1 H2;
-cases Axy (H1 H1); cases Ayz (H2 H2); [1:cases (Lxy H1)|3:cases (Lyz H2)]clear Axy Ayz;
-[1: cases (hos_cotransitive E ?? y H1) (X X); [cases (Lxy X)|cases (hos_coreflexive E ? X)]
-|2: cases (hos_cotransitive E ?? x H2) (X X); [right;assumption|cases (Lxy X)]]
-qed.
-
-theorem lt_to_excess: ∀E:ordered_set.∀a,b:E. (a < b) → (b ≰ a).
-intros (E a b Lab); cases Lab (LEab Aab); cases Aab (H H);[cases (LEab H)]
-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).