proposition: Lemma inC1_or_inC2 (l r : R) (z : C) : (inC1 l r z) || (inC2 l r z) = (inC12 l r z).
proof: Proof. by []. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol mathcomp(complex)