proposition: Lemma Mobius'M (p q : {poly R}) (l r : R) : Mobius' (p * q) l r = Mobius' p l r * Mobius' q l r.
proof: Proof. by rewrite /Mobius' !rmorphM /= reciprocalM rmorphM. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol