proposition: Lemma modn_prodm I r (P : pred I) F d : \prod_(i <- r | P i) (F i %% d) = \prod_(i <- r | P i) F i %[mod d].
proof: Proof. apply/eqP; elim/big_rec2: _ => // i m n _ /eqP nEm. by rewrite modnMml -modnMmr nEm modnMmr. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)