proposition: Lemma mono_ker (M N : {fpmod R}) (phi : 'Mono(M,N)) : is_kernel (coker phi) phi.
proof: Proof. split; first by rewrite mulmorc. move=> L X; apply: (iffP idP); last first. move=> [Y /eqmorMr /eqmor_ltrans <-]; rewrite -mulmorA. by rewrite (eqmor_ltrans (eqmorMl _ (mulmorc _))) mulmor0. rewrite /eqmor subr0 /= mulmx1 => /dvd_col_mxP [Y Ydef]. suff Ymor : pres M %| pres L *m Y. by exists (Morphism Ymor); rewrite /= -dvdmxN opprB. have := kernel_eq0 phi; rewrite /eqmor subr0 /=. move=> /dvdmx_trans -> //; rewrite dvd_ker. rewrite -mulmxA -[Y *m phi](addrNK X%:m) mulmxDr dvdmxD ?dvdmx_morphism //. by rewrite 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