proposition: Lemma rel_on_quoP p r: equivalence r -> compatible_with_equiv_p p r -> forall t, (relation_on_quotient p r t <-> (inc t (quotient r) /\ forall x, inc x t -> p x)).
proof: Proof. move=> er co t; split. move=> [tq [x xt px]]; split=>// u ut; apply: (co _ _ px). by move: tq => /(setQ_P er) h; apply /(in_class_relatedP er); exists t. move => [tq xtpx];move: (setQ_ne er tq) => /rep_i net. split =>//; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)