proposition: Lemma factorP (M N P : {fpmod R}) (phi : 'Mono(N,P)) (psi : 'Mor(M,P)) : psi ** coker phi %= 0 -> factor phi psi ** phi %= psi.
proof: Proof. have := kernel_eq0 phi; rewrite /factor. case: eqP => // phi_inj _; case: factor_proof => //= p _. by case: sig_eqW. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice matrix bigop zmodp mxalgebra poly) ssrcomplements stronglydiscrete coherent edr