proposition: Lemma olex_cc_comparable1 (r':= olex r g): (allf g total_order) -> forall x y, ocomparable r' x y <-> [/\ inc x (substrate r'), inc y (substrate r') & worder (olex_io r x y)].
proof: Proof. move: olex_osr => [or' sr]. have or: order r by move: ax => [[ ok _] _]. have aux: forall t, worder (olex_io r t t). move => t; rewrite /olex_io /olex_nsv. set Z := Zo _ _; have -> : Z = emptyset. by apply /set0_P => z /Zo_hi. have aux1: sub emptyset (substrate r) by fprops. move: (iorder_osr or aux1) => [pa pb]. split => //; rewrite pb => x xe [y yx]; move: (xe _ yx);case; case. move=> h x y. rewrite sr; split. case; move /olex_gleP => [pa pb pc]; split => //; case: pc => pc. - rewrite pc; apply: aux. - by move: pc => [wo _]. - rewrite pc; apply: aux. - by rewrite olex_ioS; move: pc => [wo _]. move=> [xp yp wot]. case: (equal_or_not x y) => xy. by left; rewrite xy; apply /olex_gleP => //;apply: olex_R. move: (olex_nsve1 xp yp xy wot). move: (olex_ioS r y x) => ppa. set i := (the_least _); move => [pa pb]. have pc: sub (olex_nsv r x y) (substrate r) by apply: Zo_S. have sd: substrate r = domain g by move: ax => [_]. have sr': substrate (olex_io r x y) = olex_nsv r x y by rewrite iorder_sr. have nsv: Vg x i <> Vg y i. by move: pa; rewrite sr' => /Zo_hi. have nsv': Vg y i <> Vg x i by apply:nesym. have pg: inc i (domain g) by rewrite - sd; apply: pc; rewrite - sr'. move: (h _ pg) => [ori tori]. have pd: order_fam g by move: ax=> [_ _]. have px: inc (Vg x i) (substrate (Vg g i)). by move: xp => /prod_of_substratesP [_ _]; apply. have py: inc (Vg y i) (substrate (Vg g i)). by move: yp => /prod_of_substratesP [_ _ ]; apply. case: (tori _ _ px py) => cp;[left | right ]. by apply /olex_gleP;split => //;right. by apply /olex_gleP;split => //; right; split => //; rewrite ppa. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)