proposition: Lemma monoP : reflect is_mono (kernel phi %= 0).
proof: Proof. apply: (iffP idP); last by apply; rewrite mulkmor. rewrite /is_mono /eqmor subr0 => /= dvdMK P psi. rewrite subr0 => dvd_phi_psi. by rewrite (dvdmx_trans dvdMK) //= subr0 dvd_ker. 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