proposition: Theorem three_circles_2 (l r : R) (p : {poly R}) (a : R) : ~~ root p r -> l < a < r -> ~~ root p a -> (forall z : C, root (toC p) z -> ~~ inC12 l r z) -> changes (seqn0 (Mobius' (p * ('X - a%:P)) l r)) = 1%N.
proof: Proof. move=> Hpnorootr /andP [] Hal Har Hpnoroota H. have Hlr : l != r by rewrite lt_eqF// (lt_trans Hal). have Hal2 : l != a by rewrite negbT // lt_eqF. have [Hp|Hp] := eqVneq p 0. have : false => //. by rewrite -(andbN (root p a)) Hpnoroota Hp root0. have Hlc1 : (lead_coef (Mobius' (R:=R) (p * ('X - a%:P)) l r))^-1 != 0. rewrite invr_neq0 // Mobius'M lead_coefM mulf_neq0 //; rewrite lead_coef_eq0 -Mobius'0 // negbT //. exact: polyXsubC_eq0. have Hl2 : lead_coef (Mobius' p l r) != 0 by rewrite lead_coef_eq0 -Mobius'0. rewrite -(@changes_nseq _ (lead_coef (Mobius' (p * ('X - a%:P)) l r)) ^-1) // seqn0_nseq // -mul_polyC_seqmul //. rewrite Mobius'M lead_coefM -mul_polyC invrM ?unitfE; [ | by [] |]; last first. by rewrite lead_coef_eq0 -Mobius'0 // negbT // polyXsubC_eq0. rewrite rmorphM /= mulrA mulrC !mulrA (mulrC (Mobius' ('X - a%:P) _ _) _) mul_polyC -mulrA mul_polyC mulrC [in X in (changes (R:=R) (seqn0 (polyseq (_ * X))))] (@Mobius'_Xsubc_monic R a l r Hlr Hal2) -(opprK ((r - a) / (l - a))%:P) -polyCN. apply: normal_changes. by rewrite oppr_gt0 pmulr_rlt0 ?invr_lt0 ?subr_lt0 // subr_gt0. apply: normal_root_inB => [ | z Hz]. rewrite monicE lead_coef_lreg. by rewrite mulrC -unitrE unitfE. exact/lregP/invr_neq0. have [/eqP Hz2|Hz2] := eqVneq (z + 1) 0. rewrite addr_eq0 in Hz2. by rewrite (eqP Hz2) inBneg1. rewrite (inB_notinC12 Hlr) //. rewrite -mul_polyC rmorphM /= map_polyC mul_polyC rootZ in Hz. apply: H. by rewrite root_Mobius'_C_2. by rewrite /= eq_complex negb_and/= invr_neq0. rewrite rootZ. rewrite -root_Mobius'_2; last by rewrite add0r oner_neq0. by rewrite mulr0 addr0 add0r invr1 mulr1. exact: invr_neq0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol mathcomp(complex)