firs step for dualization

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

diff --git a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
index 231cdf941aacb8b28d1230535901f2f691f978ef..d4aa1d57d18780367e650b63dc9ad37eb0109a72 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
@@ -44,9 +44,10 @@ cases (nat_discriminable x z); [2: left; assumption] cases H1; clear H1;
 qed.
   
 lemma nat_ordered_set : ordered_set.
-apply (mk_ordered_set ? nat_excess);
-[1: intro x; intro; apply (not_le_Sn_n ? H);
-|2: apply nat_excess_cotransitive]
+letin hos ≝ (mk_half_ordered_set nat nat_excess ? nat_excess_cotransitive);[
+  intro x; intro H; apply (not_le_Sn_n ? H);]
+constructor 1;  
+[ apply hos; | apply (dual_hos hos); | reflexivity]
 qed.
 
 interpretation "ordered set N" 'N = nat_ordered_set.
@@ -54,7 +55,7 @@ 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 ?? H);
+intros; normalize in H; apply (not_lt_to_le b a H);
 qed.
  
 lemma nat_le_to_os_le:
@@ -62,6 +63,7 @@ lemma nat_le_to_os_le:
 intros 3; apply (le_to_not_lt a b);assumption;
 qed.
 
+(*
 lemma nat_lt_to_os_lt:
   ∀a,b:nat_ordered_set.a < b → lt nat_ordered_set a b.
 intros 3; split;
@@ -73,4 +75,5 @@ lemma os_lt_to_nat_lt:
   ∀a,b:nat_ordered_set. lt nat_ordered_set a b → a < b.
 intros; cases H; clear H; cases H2;
 [2: apply H;| cases (H1 H)]
-qed.
\ No newline at end of file
+qed.
+*)
\ No newline at end of file