proposition: Lemma cokerP (M N : {fpmod R}) (phi : 'Mor(M,N)) : is_coker phi (coker phi).
proof: Proof. split; first by rewrite mulmorc. move=> L X; apply: (iffP idP) => [phiX|[Y]]; last first. move/eqmorMl/eqmor_ltrans <-; rewrite mulmorA. by rewrite (eqmor_ltrans (eqmorMr _ (mulmorc _))) mul0mor. by exists (lift phi X); rewrite mul_lift. 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