proposition: Lemma notinC_Re_lt0_1 : forall (z : C), z != l%:C -> notinC z = (Re ((r%:C - z) / (z - l%:C)) <= 0).
proof: Proof. case => a b Hab. rewrite /notinC /=. simpc. rewrite !mulrA -(mulNr (b * b) _) -mulrDl -expr2 (mulrDl r (-a) _) (mulrC r (a - l)) (mulrC (-a) _) (mulrDl _ _ r) (mulrDl _ _ (-a)) mulrNN mulrN -expr2 !addrA (addrC (a * r) _) -(addrA _ (a * r) _ ) (addrC (a * r) _ ) (mulrC a r) addrA (addrC (- l * r) _ ) -(addrA _ (r * a) (l * a)) -(mulrDl _ _ a) -(addrA (- a ^+2) _ _) (addrC (- l * r)) -!addrA (addrC _ (- b^+2)) !addrA mulNr (mulrC l r) (addrC r l) -oppr_ge0 -[X in (_ = (0 <= X))]mulNr !opprD !opprK pmulr_lge0 //. rewrite invr_gt0 lt_neqAle addr_ge0 ?sqr_ge0 // andbT eq_sym paddr_eq0 ?sqr_ge0 // negb_and !sqrf_eq0 subr_eq0. by rewrite -complexr0 eq_complex negb_and /= in Hab. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol mathcomp(complex)