proposition: Lemma partition_from_equivalence r: equivalence r -> partition_s (quotient r)(substrate r).
proof: Proof. move=> er. split; last by move=> t tq; apply: (setQ_ne er tq). split; first by apply: setU_setQ. by move=> a b /(setQ_P er) ca /(setQ_P er) cd;apply: (class_dichot er). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)