proposition: Lemma notinC_Re_lt0_2 (z : C) : z + 1 != 0 -> (notinC ((r%:C + l%:C * z) / (z + 1))) = (Re z <= 0).
proof: Proof. move=> Hz. rewrite (@notinC_Re_lt0_1 ((r%:C + l%:C * z) / (z + 1))) /=. rewrite -{1}(@mulrK _ (z+1) _ r%:C); last by rewrite unitfE. rewrite -(mulNr (r%:C + l%:C * z) _ ) -(mulrDl _ _ (z+1)^-1) mulrDr mulr1 opprD !addrA addrK -{3}(@mulrK _ (z+1) _ l%:C); last by rewrite unitfE. rewrite -(mulNr (l%:C * (z+1)) _ ) -(mulrDl _ _ (z+1)^-1) mulrDr mulr1 opprD !addrA addrK invrM. rewrite invrK !mulrA -(mulrA _ _ (z+1)) (mulrC _ (z+1)) !mulrA mulrK; last by rewrite unitfE. rewrite -mulNr -mulrDl (mulrC _ z) mulrK //. by rewrite unitfE subr_eq0 eq_sym HlrC. by rewrite unitfE subr_eq0 eq_sym HlrC. by rewrite -unitrV invrK unitfE. rewrite -subr_eq0 -{2}(@mulrK _ (z + 1) _ l%:C); last by rewrite unitfE. rewrite -mulNr -mulrDl mulrDr mulr1 opprD addrA addrK mulf_neq0 //. by rewrite subr_eq add0r eq_sym HlrC. by rewrite invr_eq0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol mathcomp(complex)