proposition: Lemma inB_inB1 : forall (z : C), inB z = inB1 (z + 1).
proof: Proof. case => a b. by rewrite /inB1 /= addrK addr0 /inB. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol mathcomp(complex)