proposition: Lemma worders_qle_total E: total_order (worders_order E).
proof: Proof. move: (worders_qle_order E) =>[or sr]. split => //; rewrite sr => x y xq yq. move:(worders_eq_equivalence E) => ee. move:(setQ_ne ee xq) (setQ_ne ee yq) => [a iax] [b iby]. move:(worders_quo_isr xq iax) (worders_quo_isr yq iby)=> aw bw. case: (order_le_total(worders_wor aw) (worders_wor bw)) => lab. by left; apply/graph_on_P1; split => //; split => //; exists a, b. by right; apply/graph_on_P1; split => //; split => //; exists b, a. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)