lebesgue completely dualized

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

diff --git a/helm/software/matita/contribs/dama/dama/ordered_set.ma b/helm/software/matita/contribs/dama/dama/ordered_set.ma
index 7008b632bb2be063a8952d1652abe4a5cdc98af6..233df16f6b2c320f7980279c5e3b9a0c31353238 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_set.ma
@@ -42,13 +42,29 @@ intro; constructor 1;
 qed.
 
 record ordered_set : Type ≝ {
-  os_l : half_ordered_set;
+  os_l_ : half_ordered_set;
   os_r_ : half_ordered_set;
-  os_with : os_r_ = dual_hos os_l
+  os_with : os_r_ = dual_hos os_l_
 }.
 
+definition os_l : ordered_set → half_ordered_set.
+intro h; constructor 1; 
+[ apply (hos_carr (os_l_ h));
+| apply (λx,y.hos_excess (os_l_ h) x y);
+| apply (hos_coreflexive (os_l_ h));
+| apply (hos_cotransitive (os_l_ h));
+]
+qed.
+
 definition os_r : ordered_set → half_ordered_set.
-intro o; apply (dual_hos (os_l o)); qed.
+intro o; apply (dual_hos (os_l_ o)); qed.
+
+lemma half2full : half_ordered_set → ordered_set.
+intro hos;
+constructor 1; [apply hos; | apply (dual_hos hos); | reflexivity] 
+qed.
+
+(* coercion half2full. *)
   
 definition Type_of_ordered_set : ordered_set → Type.
 intro o; apply (hos_carr (os_l o)); qed.