proposition: Fact mulmor_proof phi psi : pres K %| pres M *m (phi *m psi).
proof: Proof. rewrite mulmxA (dvdmx_trans (dvdmx_morphism psi)) //. by rewrite dvdmxMr // 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