proposition: Lemma mulepi_eq0 (L : {fpmod R}) (phi : 'Epi(M,N)) (Y : 'Mor(N, L)) : (phi ** Y %= 0) = (Y %= 0).
proof: Proof. apply/idP/idP; first by move/epi. by move/eqmorMl/eqmor_ltrans ->; rewrite mulmor0. 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