-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.
+
+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.
+
+(*
+lemma nat_lt_to_os_lt:
+ ∀a,b:nat_ordered_set.a < b → lt nat_ordered_set a b.
+intros 3; split;
+[1: apply nat_le_to_os_le; apply lt_to_le;assumption;
+|2: right; apply H;]
+qed.
+
+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)]