proposition: Lemma poly_split_fact p : { sq : (seq (R * nat) * {poly R}) | fact_list p (sq.1) (sq.2) & ( (p != 0 -> (forall x, 0 <x -> ~~ root (sq.2) x)) /\ (p = 0 -> sq.1 = [::] /\ sq.2 = 0)) }.
proof: Proof. case pnz: (p != 0); last first. by exists ([::],p) => //; split => //; rewrite big_nil mul1r. pose sa := [seq z <- rootsR p | 0 <z ]. pose sb := [seq (z, \mu_z p) | z <- sa]. have sav: sa = [seq z.1 | z <- sb]. by rewrite /sb - map_comp; symmetry; apply: map_id_in => a. have pa: (all (fun z => 0 < z) [seq z.1 | z <- sb]). by rewrite - sav; apply /allP => x; rewrite mem_filter => /andP []. have pb : (sorted <%R [seq z.1 | z <- sb]). rewrite - sav. by apply: sorted_filter => //; [apply: lt_trans |apply: sorted_roots]. have pc: (all (fun z => (0<z)%N ) [seq z.2 | z <- sb]). apply /allP => x /mapP [t] /mapP [z]; rewrite mem_filter => /andP [z0 z2]. move => -> -> /=; rewrite mu_gt0 //; apply: (root_roots z2). suff: { q | p = (\prod_(z <- sa) ('X - z%:P) ^+ (\mu_z p)) * q & forall x : R, 0 < x -> ~~ root q x}. move => [q qa qb]; exists (sb,q) => //. split => //;rewrite qa /= big_map; congr (_ * _); apply eq_big. by split => // pz; move: pnz; rewrite pz eqxx. clear sb sav pa pb pc. have: all (root p) sa. apply/allP=> x;rewrite mem_filter =>/andP [_]; apply /root_roots. have: uniq sa by apply:filter_uniq; apply: uniq_roots. have: forall x, root p x -> 0 < x -> (x \in sa). by move=> x rx xp;rewrite mem_filter xp -(roots_on_rootsR pnz) rx. move: sa=> s. elim: s p pnz=>[p _ H _ _| ]. exists p; first by by rewrite big_nil mul1r. move => x xp;apply/negP =>nr; by move: (H _ nr xp). move => a l Hrec /= p p0 rp /andP [nal ul] /andP [ap rap]. have [q rqa pv] := (mu_spec a p0). case q0: (q != 0); last by move:p0; rewrite pv (eqP(negbFE q0)) mul0r eqxx. have q1 x: root q x -> 0 < x -> x \in l. move=> rx xp; case xa: (x == a); first by rewrite -(eqP xa) rx in rqa. by rewrite -[_ \in _]orFb -xa -in_cons rp // pv rootM rx. have q2: all (root q) l. apply/allP=> x xl. case xa: (x ==a); first by move: nal; rewrite - (eqP xa) xl. move /(allP rap): xl. by rewrite pv rootM -[\mu__ _]prednK ?mu_gt0 // root_exp_XsubC xa orbF. have [r qv rq]:= (Hrec q q0 q1 ul q2). exists r => //; rewrite {1} pv {1} qv mulrAC; congr (_ * _). rewrite big_cons mulrC; congr (_ * _). rewrite 2! (big_nth 0) 2! big_mkord; apply: eq_bigr => i _. set b := l`_i;congr (_ ^+ _). have rb: root q b by apply /(allP q2); rewrite mem_nth //. have nr: ~~ root (('X - a%:P) ^+ \mu_a p) b. rewrite /root horner_exp !hornerE expf_neq0 // subr_eq0; apply /eqP => ab. by move: rqa; rewrite - ab rb. rewrite pv mu_mul ? (muNroot nr) // ?addn0//. by rewrite mulf_neq0 // expf_neq0 // monic_neq0 // monicXsubC. 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)