proposition: Lemma worders_qle_propc E u v: inc u (worders E) -> inc v (worders E) -> ( u <=O v <-> gle (worders_order E) (class (worders_eq E) u) (class (worders_eq E) v)).
proof: Proof. move => usr vsr. move:(worders_eq_equivalence E) => ee. move:(usr)(vsr); rewrite - worders_eq_sr => usa vsa. move: (inc_itself_class ee usa) (inc_itself_class ee vsa) => ru rv. split. move => h; apply/graph_on_P1. move: (inc_class_setQ usa) (inc_class_setQ vsa) => cqu cqv. by split => //; split => //; exists u, v. move/graph_on_P1 =>[_ _ /worders_qle_prop cp]; exact: (cp _ _ ru rv). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)