proposition: Lemma eqmorMr (psi : 'Mor(N, P)) (phi1 phi2 : 'Mor(M, N)) : phi1 %= phi2 -> phi1 ** psi %= phi2 ** psi.
proof: Proof. rewrite /eqmor=> phi12. by rewrite -mulmxBl (dvdmx_trans (dvdmx_morphism psi)) ?dvdmxMr. 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