+record half_ordered_set: Type ≝ {
+ hos_carr:> Type;
+ wloss: ∀A,B:Type. (A → A → B) → A → A → B;
+ wloss_prop: (∀T,R,P,x,y.P x y = wloss T R P x y) ∨ (∀T,R,P,x,y.P y x = wloss T R P x y);
+ hos_excess_: hos_carr → hos_carr → CProp;
+ hos_coreflexive: coreflexive ? (wloss ?? hos_excess_);
+ hos_cotransitive: cotransitive ? (wloss ?? hos_excess_)
+}.
+
+definition hos_excess ≝ λO:half_ordered_set.wloss O ?? (hos_excess_ O).
+
+(*
+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.
+*)
+
+definition dual_hos : half_ordered_set → half_ordered_set.
+intro; constructor 1;
+[ apply (hos_carr h);
+| apply (λT,R,f,x,y.wloss h T R f y x);
+| intros; cases (wloss_prop h);[right|left]intros;apply H;
+| apply (hos_excess_ h);
+| apply (hos_coreflexive h);
+| intros 4 (x y z H); simplify in H ⊢ %; cases (hos_cotransitive h y x z H);
+ [right|left] assumption;]
+qed.
+
+record ordered_set : Type ≝ {
+ os_l : half_ordered_set;
+ os_r_ : half_ordered_set;
+ os_with : os_r_ = dual_hos os_l