proposition: Lemma eqn_modDl p m n d : (p + m == p + n %[mod d]) = (m == n %[mod d]).
proof: Proof. case: d => [|d]; first by rewrite !modn0 eqn_add2l. apply/eqP/eqP=> eq_mn; last by rewrite -modnDmr eq_mn modnDmr. rewrite -(modnMDl p m) -(modnMDl p n) !mulnSr -!addnA. by rewrite -modnDmr eq_mn modnDmr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)