proposition: Lemma worders_qle_order E: order_on (worders_order E) (worders_quo E).
proof: Proof. move:(worders_eq_equivalence E) => ee. have refr: forall x, inc x (worders_quo E) -> worders_qle E x x. move => x xa; split => //; move/funI_P: xa => [z ze ->]. have zz: inc z (class (worders_eq E) z) by apply/(class_P ee); equiv_tac. exists z, z;split => //; apply: order_leR. by move: ze; rewrite worders_eq_sr => /wordersP [F _ /proj1/proj1]. move: (graph_on_sr refr). set r := (graph_on (worders_qle E) (worders_quo E)) => sr. split => //; apply: order_from_rel; split. - move => y x z [xsr ysr [a [b [ax bx leab]]]] le2. move:(le2) => [_ /(setQ_ne ee) [c cz] _]. move: (worders_qle_prop le2 bx cz) (proj32 le2)=> lebc zq. split => //; exists a,c; split => //; apply: (order_leT leab lebc). - move => x y [xsr ysr [a [b [ax bx leab]]]] le2. move: (worders_qle_prop le2 bx ax) => leba. move:(worders_quo_isr xsr ax)(worders_quo_isr ysr bx) => asr bsr. move: (worders_wor asr) (worders_wor bsr) => woa wob. exact:(worders_quo_prop xsr ysr ax bx (order_le_worA woa wob leab leba)). - by move => x y [xq yq _]; split; apply: refr. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)