proposition: Lemma Gauss_dvdp_prod p (I:eqType) (l: seq I) (F: I-> {poly R}): (all (fun i => (F i) %| p) l) -> (uniq [seq F i | i <- l]) -> (forall i j, i \in l -> j \in l -> (i == j) || coprimep (F i) (F j)) -> \prod_(i <- l) (F i) %| p.
proof: Proof. move: p; elim: l. by move => p _ _ _; rewrite big_nil dvd1p. move => a l Hrec p /= /andP [ap dr] /andP [al ul] etc. have aa: coprimep (F a) (\prod_(j <- l) F j). apply: coprimep_prod; apply /allP => x xl. have xal: x \in a :: l by rewrite inE xl orbT. have aa: F x \in [seq F i | i <- l] by apply/mapP; exists x. by move: al;case/orP: (etc _ _ (mem_head a l) xal)=> // /eqP ->; rewrite aa. rewrite big_cons Gauss_dvdp // ap /= Hrec // => i j il jl. by apply: etc; rewrite inE ? il ? jl orbT. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polydiv polyorder path interval polyrcf)