+
+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)]
+qed.
\ No newline at end of file