proposition: Lemma sub_quotient_powerset r: equivalence r -> sub (quotient r) (\Po (substrate r)).
proof: Proof. by move=> er x /(setQ_P er) => cr; apply /setP_P; apply: sub_class_sr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)