proposition: Lemma eqz_modDl p m n d : (p + m == p + n %[mod d])%Z = (m == n %[mod d])%Z.
proof: Proof. have [-> | d_nz] := eqVneq d 0; first by rewrite !modz0 (inj_eq (addrI p)). apply/eqP/eqP=> eq_mn; last by rewrite -modzDmr eq_mn modzDmr. by rewrite -(addKr p m) -modzDmr eq_mn modzDmr addKr. 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)