proposition: Lemma quo_rel_equivalence: equivalence_on (quotient_of_relations r s) (quotient s).
proof: Proof. move: (graph_ea_equivalence (proj1 (foq_finer_fs fa fe))). by rewrite/fun_on_quotient/section_canon_proj; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)