proposition: Lemma epiP : reflect is_epi (coker phi %= 0).
proof: Proof. apply: (iffP idP); last by apply; rewrite mulmorc. rewrite /is_epi /eqmor subr0. move=> /dvd_col_mxP [X /dvdmxP [Z Z_def]] P psi. rewrite !subr0 => /= /dvdmxP [Y] /(congr1 (mulmx X)). rewrite !mulmxA -[X *m phi](addrNK 1%:M) mulmxDl mul1mx. move/(canRL (addKr _)) ->. rewrite -mulNmx opprB Z_def -mulmxA dvdmxD //; last first. by rewrite mulmxA dvdmxMl. by rewrite -mulmxA dvdmxMl // dvdmx_morphism. 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