proposition: Lemma inB1_help : forall (z : C), (inB1 z) = (((Num.sqrt 3%:R) * (Re z - 1) - Im z <= 0) && (0 <= - (Num.sqrt 3%:R * (Re z - 1)) - Im z)).
proof: Proof. case=> a b. rewrite /inB1 /=. case/altP : (a - 1 =P 0) => Ha. rewrite Ha /= mulr0 oppr0 add0r lexx/= (expr2 0) !mulr0. by rewrite -eq_le oppr_eq0 -sqrf_eq0 eq_le sqr_ge0 andbT. rewrite -{1}(sqr_sqrtr (a:=3%:R)); last by apply: ler0n. rewrite -exprMn -(ler_sqrt (b^+2)). rewrite !sqrtr_sqr normrM (ger0_norm (x := Num.sqrt 3%:R)); last by apply: sqrtr_ge0. apply/idP/idP => /andP [] => H1 H2. rewrite -(normrN (a - 1)) (gtr0_norm (x:= - (a - 1))) in H2. by rewrite ler_norml mulrN opprK -subr_le0 -[X in (_ && X)]subr_ge0 in H2. by rewrite oppr_gt0 lt_def H1 eq_sym Ha. have Hb : `|b| <= Num.sqrt 3%:R * -(a - 1). by rewrite ler_norml mulrN opprK -subr_le0 -[X in (_ && X)]subr_ge0 H1 H2. have Ha2 : (0 <= - (a - 1)). rewrite -(pmulr_lge0 (x:=Num.sqrt 3%:R)); last by rewrite sqrtr_gt0 ltr0n. by rewrite mulrC (@le_trans _ _ `| b |). by rewrite -oppr_ge0 Ha2 /= -(normrN (a-1)) (ger0_norm (x:= -(a-1))). rewrite exprMn mulr_gt0 // lt_def sqr_ge0. by rewrite sqrf_eq0 sqrtr_eq0 -ltNge ltr0n. by rewrite sqrf_eq0 Ha. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol mathcomp(complex)