proposition: Lemma divn_mulAC d m n : d %| m -> m %/ d * n = m * n %/ d.
proof: Proof. case: d m => [[] //| d m] dv_d_m; apply/eqP. by rewrite eqn_div ?dvdn_mulr // mulnAC divnK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)