proposition: Lemma inBneg1 : @inB R (-1).
proof: Proof. by rewrite /inB !raddfN lerN10 /= oppr0 sqrrN !expr2 mulr0 !mulr1 ler0n. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol mathcomp(complex)