proposition: Lemma worders_eq_compat_le E a b c d: related (worders_eq E) a b -> related (worders_eq E) c d -> (a <=O c <-> b <=O d).
proof: Proof. move => /graph_on_P0 [_ _ is1] /graph_on_P0 [_ _ is2]. exact: (order_le_compatible is1 is2). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)