proposition: Lemma modnMDl p m d : p * d + m = m %[mod d].
proof: Proof. have [->|d_gt0] := posnP d; first by rewrite muln0. by rewrite [in LHS](divn_eq m d) addnA -mulnDl modn_def edivn_eq // ltn_mod. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)