X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fordered_set.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fordered_set.ma;h=233df16f6b2c320f7980279c5e3b9a0c31353238;hb=82d281529c1a9450ac213a058e7f8c0e228026fa;hp=7008b632bb2be063a8952d1652abe4a5cdc98af6;hpb=04c05cf08605156ba8c6fa7225b4a90496c03698;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/ordered_set.ma b/helm/software/matita/contribs/dama/dama/ordered_set.ma
index 7008b632b..233df16f6 100644
--- 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.