qed.
lemma nat_ordered_set : ordered_set.
-letin hos ≝ (mk_half_ordered_set nat (λT:Type.λf:T→T→CProp.f) ? nat_excess ? nat_excess_cotransitive);
+letin hos ≝ (mk_half_ordered_set nat (λT,R:Type.λf:T→T→R.f) ? nat_excess ? nat_excess_cotransitive);
[ intros; left; intros; reflexivity;
| intro x; intro H; apply (not_le_Sn_n ? H);]
constructor 1;