-(*
-lemma find_leq : half_ordered_set → half_ordered_set.
-intro O; constructor 1;
-[1: apply (hos_carr O);
-|2: apply (λT:Type.λf:T→T→CProp.f);
-|3: intros; left; intros; reflexivity;
-|4: apply (hos_excess_ O);
-|5: intro x; lapply (hos_coreflexive O x) as H; cases (wloss_prop O);
- rewrite < H1 in H; apply H;
-|6: intros 4 (x y z H); cases (wloss_prop O);
- rewrite > (H1 ? (hos_excess_ O)) in H ⊢ %;
- rewrite > (H1 ? (hos_excess_ O)); lapply (hos_cotransitive O ?? z H);
- [assumption] cases Hletin;[right|left]assumption;]
-qed.
-*)
-