proposition: Lemma Bernstein_isolate deg a b (l : {poly R}): a < b -> (0 < size l)%N -> (size l <= deg.+1)%N -> alternate (Mobius deg a b l) -> one_root1 l a b.
proof: Proof. rewrite /Mobius /recip => altb s0 sz. have sss : size ((l \shift a) \scale (b - a)) = size l. rewrite size_scaleX; last by move: altb; rewrite -subr_gt0 lt0r; case/andP. by rewrite size_comp_poly2 // size_XaddC. rewrite sss => alt. have -> : a = a + (a - a) by rewrite addrN addr0. have -> : b = a + (b - a) by rewrite (addrC b) addNKr. apply: one_root1_shift. rewrite addrN -(mulr1 (b - a)) -(mulr0 (b - a)). apply: one_root1_scale; first by rewrite subr_gt0. move/desc: alt => alt'; move/one_root2_shift: alt'; rewrite addr0 -sss. by apply: one_root_reciprocal; rewrite sss. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol