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