proposition: Lemma coprimepMr p q r : coprimep p (q * r) = (coprimep p q && coprimep p r).
proof: Proof. apply/coprimepP/andP=> [hp | [/coprimepP-hq hr]]. by split; apply/coprimepP=> d dp dq; rewrite hp //; [apply/dvdp_mulr | apply/dvdp_mull]. move=> d dp dqr; move/(_ _ dp) in hq. rewrite Gauss_dvdpl in dqr; first exact: hq. by move/coprimep_dvdr: hr; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)