proposition: Lemma Gauss_dvdp_prod2 p (l: seq (R * nat)): (all (fun z => ('X - z.1%:P)^+ (z.2) %| p) l) -> (uniq [seq z.1 | z <- l]) -> \prod_(i <- l) ('X - i.1%:P)^+ (i.2) %| p.
proof: Proof. move => pa pb. set l2:= [seq z <- l | z.2 != 0%N]. have qc: all (fun z => z.2 !=0%N) l2 by apply: filter_all. have qa:all (fun z => ('X - (z.1)%:P) ^+ z.2 %| p) l2. by apply /allP => x; rewrite mem_filter => /andP [_] /(allP pa). have qb: uniq [seq z.1 | z <- l2]. move: pb;rewrite /l2; elim l => [|x s IHs] //= /andP [Hx Hs]. case (x.2 == 0%N); rewrite /= IHs // andbT; apply /negP. move /mapP => [y]; rewrite mem_filter => /andP [_ ys] xy. move: Hx; rewrite xy; move/negP;case; apply /mapP; exists y => //. have ->: \prod_(i <- l) ('X - (i.1)%:P) ^+ i.2 = \prod_(i <- l2) ('X - (i.1)%:P) ^+ i.2. rewrite big_filter [X in _ = X] big_mkcond /=; apply: eq_bigr => i _. by case h: (i.2 == 0%N) => //=; rewrite (eqP h) expr0. apply:Gauss_dvdp_prod => //. rewrite map_inj_in_uniq. apply: (map_uniq qb). move => i j il jl /= eq1. rewrite (surjective_pairing i) (surjective_pairing j). move: (size_exp_XsubC i.2 (i.1)); rewrite eq1 size_exp_XsubC. move /eq_add_S => ->. have: root (('X - (i.1)%:P) ^+ i.2) (i.1). move: (allP qc _ il); rewrite -lt0n => /prednK <-. by rewrite root_exp_XsubC eqxx. rewrite eq1; move: (allP qc _ jl); rewrite -lt0n => /prednK <-. by rewrite root_exp_XsubC => /eqP ->. move => i j il2 jl2. pose zz:(R * nat) := (0, 0%N). move: (nth_index zz il2)(nth_index zz jl2). move: il2 jl2; rewrite -(index_mem) -(index_mem). set i1 := index i l2; set j1 := index j l2 => ra rb rc rd. set l3 := [seq z.1 | z <- l2]. have ss: size l2 = size l3 by rewrite /l3 size_map. move: (ra) (rb);rewrite ss => ra' rb'. move: (nth_uniq 0 ra' rb' qb) => aux. case eqq: (i1 == j1). by rewrite - rc - rd (eqP eqq) eqxx. apply /orP; right. rewrite coprimep_expl // coprimep_expr // coprimep_XsubC root_XsubC. by rewrite - rc - rd -(nth_map zz 0) // -(nth_map zz 0) // -/l3 eq_sym aux eqq. 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)