proposition: Lemma coprimep_prod p I l (F: I-> {poly R}): (all (fun z => coprimep p (F z)) l) -> coprimep p (\prod_(z <- l) (F z)).
proof: Proof. elim l; first by rewrite big_nil /= coprimep1. by move => b m Hrec /andP [ap /Hrec]; rewrite big_cons coprimepMr ap => ->. 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)