proposition: Lemma root_Mobius'_2 (p : {poly R}) (x : R) (l r : R) : x + 1 != 0 -> root p ((r + l * x) / (x + 1)) = root (Mobius' p l r) x.
proof: Proof. move=> Hx. rewrite /Mobius -root_shift_2 -root_reciprocal_2 //. rewrite -root_scale_2 -root_shift_2 -{3}(@mulrK _ (x + 1) _ l). by rewrite -mulrDl {2}(@addrC _ x 1) mulrDr mulr1 addrA -(addrA r (- l) l) (addrC (-l) l) addrA addrK. by rewrite unitfE. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol