proposition: Lemma Mobius'_Xsubc (c l r : R) : (l != r) -> Mobius' ('X - c%:P) l r = (l - c) *: 'X + (r - c)%:P.
proof: Proof. move=> Hlr. rewrite /Mobius' rmorphB /= shift_polyC rmorphB /= scaleX_polyC /shift_poly comp_polyX rmorphD /= scaleX_polyC /scaleX_poly comp_polyX -addrA -(rmorphB _ l c) /= reciprocal_monom. by rewrite rmorphD rmorphM /= comp_polyX !comp_polyC mulrDl polyC1 mul1r mulrC mul_polyC -addrA (addrC (l - c)%:P _) -rmorphD /= addrA addrNK. by rewrite subr_eq0 eq_sym. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol