proposition: Lemma quot_kernel_can': cancel (fun b => \pi f' b) (fun c => f (@repr _ r c)).
proof: Proof. intro. by rewrite surj_repr_pi. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij)