proposition: Lemma eqz_mod_dvd d m n : (m == n %[mod d])%Z = (d %| m - n)%Z.
proof: Proof. apply/eqP/dvdz_mod0P=> eq_mn. by rewrite -modzDml eq_mn modzDml subrr mod0z. by rewrite -(subrK n m) -modzDml eq_mn add0r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly ssrnum ssrint archimedean rat matrix) mathcomp(polydiv perm zmodp mxalgebra vector)