proposition: Lemma dvdn_divRL p d m : p %| m -> (d %| m %/ p) = (d * p %| m).
proof: Proof. have [-> | /(@dvdn_pmul2r p d) <- /divnK-> //] := posnP p. by rewrite divn0 muln0 dvdn0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)