-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 nat_excess ? nat_excess_cotransitive);[
+ intro x; intro H; apply (not_le_Sn_n ? H);]
+constructor 1;
+[ apply hos; | apply (dual_hos hos); | reflexivity]
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.
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.
∀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)]
∀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)]