proposition: Lemma divp_mulAC d m n : d %| m -> m %/ d * n = m * n %/ d.
proof: Proof. by move=> hdm; rewrite mulrC (mulrC m); apply: divp_mulA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)