proposition: Lemma prev_rootM a b (p q : {poly R}) : prev_root (p * q) a b = maxr (prev_root p a b) (prev_root q a b).
proof: Proof. apply/esym/is_prev_root. wlog: p q / prev_root p a b >= prev_root q a b. case: leP=> hpq; last by move/(_ _ _ (ltW hpq)); case: leP hpq. by move/(_ _ _ hpq); case: ltP hpq; rewrite mulrC. case: ltP => //; case: (@prev_rootP p)=> [|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: prev_rootP hpq; rewrite // (itvP hy). - by rewrite hornerM py0 mul0r. - move=> z hz /=; rewrite rootM negb_or ?hp //. by rewrite (@prev_noroot _ a b) //; apply: subitvPl hz. * case: (eqVneq q 0) hpq => [->|q0 hpq]. rewrite mulr0 root0 prev_root0 le_minr lexx andbT. by move/min_r->; constructor. constructor=> //; first by rewrite mulf_neq0. move=> z hz /=; rewrite rootM negb_or ?hp // (@prev_noroot _ a b) //. by apply: subitvPl hz=> /=; move: hpq; rewrite le_minr; 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)