proposition: Lemma worder_in_class_pr E x a: inc x (worders_quo E) -> inc a x -> x = class (worders_eq E) a.
proof: Proof. move: (worders_eq_equivalence E) => ee. move => /funI_P[b bsr ->] /(class_P ee) rba. by apply: (class_eq1 ee). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)