proposition: Lemma Mobius'_toC (p : {poly R}) (l r : R) : toC (Mobius' p l r) = Mobius' (toC p) l%:C r%:C.
proof: Proof. by rewrite {2}/Mobius' -shift_toC /= -rmorphB -scale_toC -reciprocal_toC -shift_toC /Mobius. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol mathcomp(complex)