proposition: Lemma factor_proof (M N P : {fpmod R}) (phi : 'Mono(N,P)) (psi : 'Mor(M,P)) : reflect (exists kapa, kapa ** phi %= psi) (psi ** coker phi %= 0).
proof: Proof. apply: (iffP idP) => [|[c]]; last first. move/eqmorMr/eqmor_ltrans <-; rewrite -mulmorA. by rewrite (eqmor_ltrans (eqmorMl _ (mulmorc _))) mulmor0. rewrite /eqmor /= subr0 mulmx1 => /dvd_col_mxP [X Xdef]. suff Xmor : pres N %| pres M *m X. by exists (Morphism Xmor); rewrite -dvdmxN opprB. have /monoP := @mono _ _ _ phi. rewrite /eqmor /= subr0 => /dvdmx_trans -> //. rewrite dvd_ker -mulmxA -[X *m _](addrNK psi%:m). by rewrite mulmxDr dvdmxD ?dvdmx_morphism // dvdmxMl // -dvdmxN opprB. 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