proposition: Lemma eqmor_trans : transitive eqmor.
proof: Proof. rewrite /eqmor => phi2 phi1 phi3 phi12 phi23. by rewrite -[phi1%:m](addrNK phi2%:m) -[X in _ %| X]addrA dvdmxD. 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