ordered_set simplified

[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 e7dfec46152d1ef9cb32951cc9e7a4df2bfc8f4e..26e2f0d2953a75ac9e3706babd7ec22a3b4f695d 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
@@ -12,10 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ordered_set.ma".
-
 include "nat/compare.ma".
-include "cprop_connectives.ma".
+include "bishop_set.ma". 
 
 definition nat_excess : nat → nat → CProp ≝ λn,m. m<n.
 
@@ -27,6 +25,7 @@ intros 5;elim n; [apply H]
 cases m;[ apply H1| apply H2; apply H3 ]
 qed.
 
+alias symbol "lt" = "natural 'less than'".
 lemma nat_discriminable: ∀x,y:nat.x < y ∨ x = y ∨ y < x.
 intros (x y); apply (nat_elim2 ???? x y); 
 [1: intro;left;cases n; [right;reflexivity] left; apply lt_O_S;
@@ -45,7 +44,22 @@ 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 (λT,R:Type.λf:T→T→R.f) ? nat_excess ? nat_excess_cotransitive);
+[ intros; left; intros; reflexivity;
+| intro x; intro H; apply (not_le_Sn_n ? H);]
+constructor 1;  apply hos;
+qed.
+
+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 b a H);
+qed.
+ 
+lemma nat_le_to_os_le:
+  ∀a,b:nat_ordered_set.le a b → a ≤ b.
+intros 3; apply (le_to_not_lt a b);assumption;
 qed.
+