proposition: Lemma quot_kernel_can: cancel (fun c => f (@repr _ r c)) (fun b => \pi f' b).
proof: Proof. intro. rewrite -{2}(reprK x); apply /eqquotP. by apply/Hr. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij)