proposition: Lemma kernel_equivalence A (B : eqType) (f : A -> B) : equiv_class_of (kernelb f).
proof: Proof. by split => [x|x y|x y z] //= => /eqP->/eqP->. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij)