proposition: Lemma next_rootM a b (p q : {poly R}) : next_root (p * q) a b = minr (next_root p a b) (next_root q a b).
proof: Proof. apply/esym/is_next_root. wlog: p q / next_root p a b <= next_root q a b. case: leP=> hpq; first by move/(_ _ _ hpq); case: leP hpq. by move/(_ _ _ (ltW hpq)); rewrite mulrC; case: ltP hpq. case: leP => //; case: next_rootP=> [|y np0 py0 hy|c np0 ->] hp hpq _. * by rewrite hp mul0r root0; constructor. * rewrite rootM; move/rootP:(py0)->; constructor=> //. - by rewrite mulf_neq0 //; case: next_rootP hpq; rewrite // (itvP hy). - by rewrite hornerM py0 mul0r. - move=> z hz /=; rewrite rootM negb_or ?hp //. by rewrite (@next_noroot _ a b) //; apply: subitvPr hz. * case: (eqVneq q 0) hpq => [->|q0 hpq]. rewrite mulr0 root0 next_root0 le_maxl lexx andbT. by move/max_r->; constructor. constructor=> //; first by rewrite mulf_neq0. move=> z hz /=; rewrite rootM negb_or ?hp // (@next_noroot _ a b) //. by apply: subitvPr hz=> /=; move: hpq; rewrite le_maxl; case/andP. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg poly polydiv ssrnum zmodp) mathcomp(polyorder path interval ssrint)