proposition: Lemma irreducible_dvdp_seq (p r : {poly R}) s : irreducible_poly p -> p \is monic -> (dvdp p r) -> (forall q, q \in s -> irreducible_poly q) -> (forall q, q \in s -> q \is monic) -> r = \prod_(t <- s) t -> p \in s.
proof: Proof. move=> pIrr pm. elim: s r => [r pdvr _ _|a l IHl r pdvr Irr mon]. rewrite big_nil=> eqr1; move: pdvr pIrr. rewrite eqr1 dvdp1 /irreducible_poly=> /eqP ->. by rewrite ltnn; case. rewrite big_cons=> eqrM; move: pdvr; rewrite eqrM=> pdvM. case/boolP: (eqp p a)=>[|neqdpa]. have am: a \is monic by apply: mon; rewrite mem_head. by rewrite eqp_monic // => /eqP ->; rewrite mem_head. have Hia: irreducible_poly a by apply: Irr; rewrite mem_head. have cppa := coprimep_irreducible neqdpa pIrr Hia. rewrite (Gauss_dvdpr _ cppa) in pdvM. apply/mem_behead/(IHl _ pdvM)=> // q qinl. by apply: Irr; rewrite mem_behead. by rewrite mon // mem_behead. Qed.
imports: mathcomp(all_ssreflect all_algebra)