proposition: Lemma muln_modr p m d : p * (m %% d) = (p * m) %% (p * d).
proof: Proof. have [->//|p_gt0] := posnP p; apply: (@addnI (p * (m %/ d * d))). by rewrite -mulnDr -divn_eq mulnCA -(divnMl p_gt0) -divn_eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)