proposition: Lemma pos_root_deriv p: ((npos_roots p) <= (npos_roots p^`()).+1) %N.
proof: Proof. case (npos_roots0 p); last by move => ->. move => [pnz dnz]. move: (pos_split1 pnz) => [[pa pb pc pd] pe pf]. set s := pos_roots p; set q := pos_cofactor p. move: (erefl (pos_roots p)); rewrite -{2} /s; case s. by rewrite /npos_roots;move => ->; rewrite big_nil. move=> a l eq1. set r:= [seq z.1 | z <- s]; set r1:= a.1; set rs:= [seq z.1 | z <- l]. set rd:= [seq z.2 | z <- pos_roots p]. have ss: size s = (size l).+1 by rewrite /s eq1. pose zz:(R * nat) := (0, 0%N). have p0: forall i, (i < size s)%N -> (nth zz s i).2 \in rd. move => i qis; apply /mapP; exists (nth zz s i)=> //. by apply /(nthP zz); exists i. have p1: forall i: 'I_(size l)%N, {c : R | c \in `] ((r1::rs)`_i), (rs`_i)[ & (p^`()).[c] = 0}. move: pc;rewrite eq1 /=; move /(pathP 0); rewrite size_map => h. move => [i isl]; move: (h _ isl); rewrite -/r1 -/rs => lt1. have ha: forall j, (j< size s)%N -> (root p (r1 :: rs)`_j). move => j js; rewrite pa rootM /root horner_prod; apply /orP; left. rewrite (big_nth zz) big_mkord -/s (bigD1 (Ordinal js)) //= {1} /s eq1 /=. rewrite horner_exp hornerXsubC -(nth_map _ 0) /= -?ss // subrr expr0n. by rewrite (gtn_eqF (allP pd _ (p0 _ js))) mul0r eqxx. have rp: p.[(a.1 :: rs)`_i] = p.[rs`_i]. have ->: rs`_i = (r1 :: rs)`_(i.+1) by []. by rewrite (eqP (ha _ _ )) ? (eqP (ha _ _ )) //; rewrite ss ltnS // ltnW. exact: (rolle lt1 rp). set l2 := [seq (s2val (p1 i), 1%N) | i <- (enum 'I_(size l)) ]. set l3 := [seq (z.1, z.2.-1) | z <- pos_roots p]. set f2 := \prod_(z <- l2) ('X - (z.1)%:P) ^+ (z.2). set f3 := \prod_(z <- l3) ('X - (z.1)%:P) ^+ (z.2). have p2: forall t, (t < size s)%N -> (r1 :: rs)`_t = (nth zz s t).1. by move => t ts; rewrite - (nth_map zz 0) // /s eq1. have ->: (npos_roots p = (\sum_(i <- l2++l3)i.2).+1)%N. rewrite big_cat - addSn /l3 /l2 ! big_map sum1_card cardE size_enum_ord - ss. rewrite - (sum1_size s) -/s - big_split /=. rewrite /npos_roots ! (big_nth zz) ! big_mkord; apply: eq_bigr. by move => [i iv] _; rewrite add1n (prednK (allP pd _ (p0 _ iv))). have p4: (all (fun z => 0 < z) [seq z0.1 | z0 <- l2 ++ l3]). have aa: forall t, t \in s -> 0 < t.1. by move => t ts; apply: (allP pb); apply /mapP; exists t. apply /allP => x /mapP [y]; rewrite mem_cat => /orP []; last first. by move/mapP => [t /aa h -> ->]. move/mapP => [t] _ -> -> /=; move: (s2valP (p1 t)). rewrite itv_boundlr => /= /andP [lt1 _]; apply: lt_trans lt1. have ts: (t < size s)%N by rewrite /s eq1 /= ltnS ltnW. by rewrite (p2 _ ts); apply: aa;rewrite mem_nth. have pcc: forall i j, (i <size s)%N -> (j <size s)%N -> (nth zz s i).1 < (nth zz s j).1 -> (i < j)%N. move => i j il jl;case (ltngtP j i) => //; last by move => ->; rewrite ltxx. rewrite - (lt_asym (nth zz s i).1 (nth zz s j).1); move => ij -> /=. move: pc;rewrite -p2 // - p2 // eq1; set s1 := [seq z.1 | z <- a::l] => ha. have ss1 : size s = size s1 by rewrite /s1 ss size_map. rewrite ss1 in il jl; exact: (sorted_prop ha jl il ij). have p5: f3 %| p^`(). apply:Gauss_dvdp_prod2. apply /allP => x /mapP [y ys -> /=]. have: (('X - (y.1)%:P) ^+ y.2) %| p. rewrite pa; apply:dvdp_mulr. move: (nth_index zz ys) => h; move: ys; rewrite - index_mem => ys. by rewrite (big_nth zz) big_mkord (bigD1 (Ordinal ys)) //= h dvdp_mulIl. move /dvdpP => [q1 ->]; rewrite derivM; apply:dvdp_add;apply:dvdp_mull. set e := y.2; case e => // n /=; rewrite exprS; apply : dvdp_mulIr. rewrite deriv_exp - mulrnAl; apply : dvdp_mulIr. rewrite /l3 -/s -map_comp. apply: sorted_uniq. exact: lt_trans. exact: ltxx. by apply: pc. have xx: forall i: 'I_ (size l), [/\ (i <= size l)%N, (i < size s)%N & (i.+1 < size s)%N]. by move => i; rewrite ss !ltnS ltnW. have p6: f2 %| p^`(). apply:Gauss_dvdp_prod2. apply/allP => x /mapP [t] _ -> /=; move: (s2valP' (p1 t)). by rewrite dvdp_XsubCl /root=> ->; rewrite eqxx. have ->:[seq z.1 | z <- l2] = [seq s2val (p1 i)| i <- enum 'I_(size l)]. by rewrite /l2 - map_comp. rewrite map_inj_uniq; first by apply: enum_uniq. move => i j /= h. move: (xx i) (xx j)=> [isl1 isl isl2] [jsl1 jsl jsl2]. apply: val_inj => /=; apply: anti_leq. move: (s2valP (p1 i)) (s2valP (p1 j)); rewrite !itv_boundlr => /=. rewrite h; move/andP => [lt1 lt2] /andP [lt3 lt4]. move: (lt_trans lt1 lt4) (lt_trans lt3 lt2). have ->: rs`_i = (r1 :: rs)`_(i.+1) by []. have ->: rs`_j = (r1 :: rs)`_(j.+1) by []. rewrite !p2 // ? ss ? ltnS //. move /(pcc _ _ isl jsl2) => sa /(pcc _ _ jsl isl2). by rewrite ltnS => ->; rewrite -ltnS sa. have p7: coprimep f2 f3. apply: coprimep_prod; apply /allP => x xl3. rewrite coprimep_sym; apply /coprimep_prod; apply /allP => y yl2. apply:coprimep_expl; apply: coprimep_expr. rewrite coprimep_XsubC root_XsubC; apply /negP => /eqP. move: xl3 => /mapP [k ks] -> /=. rewrite - (nth_index zz ks) -/s; set kis := (index k s). move: yl2; move /mapP => [i] _ -> /= h1. move: (s2valP (p1 i)); rewrite !itv_boundlr => /=; rewrite h1; clear h1. have ->: rs`_i = (r1 :: rs)`_(i.+1) by []. move: (xx i) => [il0 il1 il2]. have il3: (kis < size s)%N by rewrite index_mem. rewrite ! p2 // => /andP [la lb]. move: (pcc _ _ il1 il3 la) (pcc _ _ il3 il2 lb). by rewrite ltnS => lc ld; move: (leq_trans lc ld); rewrite ltnn. have : (f2 * f3) %| p^`() by rewrite Gauss_dvdp // p6 p5. move /dvdpP => [q1]; rewrite mulrC => sd. have sa: p^`() = \prod_(z <- l2++l3) ('X - (z.1)%:P) ^+ z.2 * q1. by rewrite big_cat. move: (pos_split1 dnz) => [[qa qb qc qd] qe qf]. set Fa := \prod_(z <- l2 ++l3) ('X - (z.1)%:P) ^+ z.2. set Fb := \prod_(z <- pos_roots p^`()) ('X - (z.1)%:P) ^+ z.2. set q2:= pos_cofactor p^`(). have Fbm: Fb \is monic by apply:monic_prod_XsubCe. suff cp: coprimep Fa q2. move: (Gauss_dvdpl Fb cp); rewrite - qa {1} sa dvdp_mulIl => h. move: (dvdp_leq (monic_neq0 Fbm) (esym h)). by rewrite /npos_roots ! size_prod_XsubCe. rewrite/Fa coprimep_sym;apply/coprimep_prod /allP => x xl. rewrite coprimep_expr// coprimep_XsubC qe //. by apply (allP p4); apply /mapP; exists x. 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)