proposition: Lemma Gauss_dvdr m n p : coprime m n -> (m %| n * p) = (m %| p).
proof: Proof. case: n => [|n] co_mn; first by case: m co_mn => [|[]] // _; rewrite !dvd1n. by symmetry; rewrite mulnC -(@dvdn_pmul2r n.+1) ?Gauss_dvd // andbC dvdn_mull. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)