proposition: Lemma divnMDl q m d : 0 < d -> (q * d + m) %/ d = q + m %/ d.
proof: Proof. move=> d_gt0; rewrite [in LHS](divn_eq m d) addnA -mulnDl. by rewrite /divn edivn_eq // modn_def; case: edivnP; rewrite d_gt0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)