proposition: Lemma Mobius'0 (p : {poly R}) (a b : R) : a != b -> (p == 0) = ((Mobius' p a b) == 0).
proof: Proof. move=> ab; apply/idP/idP => /eqP Hp. by rewrite /Mobius' Hp /shift_poly /scaleX_poly !comp_polyC reciprocalC comp_polyC. rewrite /Mobius' in Hp. rewrite (shift_poly_eq p 0 a) shift_polyC (@scale_poly_eq _ _ (b - a)). by rewrite /scaleX_poly comp_polyC -reciprocal0 (shift_poly_eq _ _ 1) shift_polyC Hp. 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