proposition: Lemma root_Mobius'_C_2 (p : {poly R}) (z : C) (l r : R) : z + 1 != 0 -> root (toC p) ((r%:C + l%:C * z) / (z + 1)) = root (toC (Mobius' p l r)) z.
proof: Proof. move=> Hz. rewrite !rootE Mobius'_toC /Mobius -!rootE -root_shift_2 -root_reciprocal_2 //. rewrite -root_scale_2 -root_shift_2 -{3}(@mulrK _ (z + 1) _ l%:C). by rewrite -mulrDl {2}(@addrC _ z 1) mulrDr mulr1 addrA -(addrA r%:C (- l%:C) l%:C) (addrC (-l%:C) l%:C) 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 mathcomp(complex)