include "ordered_set.ma".
include "nat/compare.ma".
-include "cprop_connectives.ma".
+include "cprop_connectives.ma".
definition nat_excess : nat → nat → CProp ≝ λn,m. m<n.
[1: intro x; intro; apply (not_le_Sn_n ? H);
|2: apply nat_excess_cotransitive]
qed.
+
+alias id "le" = "cic:/matita/dama/ordered_set/le.con".
+lemma os_le_to_nat_le:
+ ∀a,b:nat_ordered_set.le nat_ordered_set a b → a ≤ b.
+intros; normalize in H; apply (not_lt_to_le ?? H);
+qed.
+
+lemma nat_le_to_os_le:
+ ∀a,b:nat_ordered_set.a ≤ b → le nat_ordered_set a b.
+intros 3; apply (le_to_not_lt a b);assumption;
+qed.
+
\ No newline at end of file