proposition: Theorem three_circles_1 (p : {poly R}) : (forall (z : C), root (toC p) z -> (notinC z)) -> changes (Mobius' p l r) = 0%N.
proof: Proof. move=> H. have [/eqP|Hp0] := eqVneq p 0. rewrite (@Mobius'0 _ p l r) ?lt_eqF// => /eqP ->. by rewrite polyseq0. rewrite (@changes_mulC R (Mobius' p l r) (lead_coef (Mobius' p l r))^-1). apply: monic_roots_changes_eq0 => [ | z Hz]. by rewrite monicE lead_coefZ mulrC -unitrE unitfE lead_coef_eq0 -Mobius'0 ?lt_eqF// Hp0. case/altP : (z+1 =P 0) => [/eqP Hz2 | Hz2]. rewrite addr_eq0 eq_complex in Hz2. move/andP : Hz2; case => /eqP Hrez _. by rewrite Hrez raddfN lerN10. rewrite map_polyZ rootZ /= -?root_Mobius'_C_2 // in Hz. rewrite -notinC_Re_lt0_2 //. apply: H => //. rewrite -complexr0 eq_complex /= negb_and eq_refl orbF. by rewrite invr_eq0 lead_coef_eq0 -Mobius'0 ?lt_eqF// negbT. by rewrite invr_eq0 lead_coef_eq0 -Mobius'0 ?lt_eqF// negbT. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol mathcomp(complex)