proposition: Lemma olex_cc_comparable2 (r':= olex r g): (allf g total_order) -> transitive_r (ocomparable r').
proof: Proof. move=> h y x z; rewrite ! (olex_cc_comparable1 h). move=> [xE yE wo1] [_ zE wo2]; split => //. move: wo1 wo2; rewrite /olex_io. apply: union2_wor. - by move: ax => [ok _]. - apply: Zo_S. - apply: Zo_S. - rewrite /olex_nsv => t /Zo_P [pa pb]. case: (equal_or_not (Vg x t) (Vg y t)) => sv. apply /setU2_P; right; apply /Zo_P;split => //; ue. by apply /setU2_P; left; apply /Zo_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)