|2: apply nat_excess_cotransitive]
qed.
+notation "\naturals" non associative with precedence 90 for @{'nat}.
+interpretation "ordered set N" 'nat = 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.