proposition: Lemma epi_coker (M N : {fpmod R}) (phi : 'Epi(M,N)) : is_coker (kernel phi) phi.
proof: Proof. split; first by rewrite mulkmor. move=> L psi; apply: (iffP idP); last first. move=> [Y /eqmorMl /eqmor_ltrans <-]; rewrite mulmorA. by rewrite (eqmor_ltrans (eqmorMr _ (mulkmor _))) mul0mor. move/mul_lift; have /mul_lift := mulkmor phi. set phi' := lift _ phi; set psi' := lift _ psi. move=> phi'E psi'E. have phi'_mono : is_mono phi' by apply: lift_mono. have phi'_epi : is_epi phi' by apply: lift_epi; rewrite mulkmor. set phi'' := @iso_of_me _ _ _ phi' phi'_mono phi'_epi. exists (phi''^^-1 ** psi'). rewrite -(eqmor_ltrans (eqmorMr _ phi'E)) -(eqmor_rtrans psi'E). rewrite -mulmorA eqmorMl // mulmorA. by rewrite (eqmor_ltrans (eqmorMr _ (mulmorV phi''))) mul1mor. 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