-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;