proposition: Lemma inB_notinC12 (l r : R) (z : C) : l != r -> z + 1 != 0 -> inB z = ~~ inC12 l r ((r%:C + l%:C * z) / (z + 1)).
proof: Proof. move=> Hlr Hz. have H : (r%:C + l%:C * z) / (z + 1) = ((r - l)%:C / (z + 1) + l%:C). rewrite -{2}[l%:C](@mulrK _ (z + 1)); last by rewrite unitfE. by rewrite -mulrDl {2}[z+1]addrC mulrDr mulr1 rmorphB /= !addrA addrNK. by rewrite H -notinC12lr_shift // -notinC1201_lr_scale // -inB1_notinC1201 // -inB_inB1. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol mathcomp(complex)