proposition: Lemma inB1_notinC1201 : forall (z : C), z != 0 -> inB1 z = ~~ inC12 0 1 (z ^-1).
proof: Proof. case=> a b Hz. rewrite -inC1_or_inC2 negb_or inB1_help /=. have H : a ^+ 2 + b ^+ 2 \is a GRing.unit. rewrite eq_complex /= negb_and in Hz. case/orP: Hz=> H; by rewrite unitfE paddr_eq0 ?sqr_ge0 // negb_and !sqrf_eq0 H ?orbT. have H3 : (Num.ExtraDef.sqrtr (GRing.natmul (V:=R) (GRing.one R) (3))) \is a GRing.unit. by rewrite unitfE sqrtr_eq0 -ltNge ltr0n. rewrite /inC1 /= -leNgt add0r oppr0 mul0r !addr0 !mul1r. rewrite [x in (0 <= ((x + _) + _))]addrC -[x in (0 <= (x + _))]addrA exprMn -(mulNr b) exprMn sqrrN -mulrDl (expr2 ((a^+2 + b^+2)^-1)) -{2}(mulr1 (a^+2 + b^+2)) -invrM // -mulf_div [x in (0 <= _ + x + _)]mulrC !mulrA (mulrK (x:=(a^+2 + b^+2))) //. rewrite -[in x in _ = x](mulNr a) -mulrDl. rewrite -{5}(opprK 1) -(opprD a (- 1)) -mulrA -invrM //. rewrite -[in x in _ = x]mulNr -(mul1r ( - (a - 1) / (a ^+ 2 + b ^+ 2))) -{5}(@mulrK _ (Num.sqrt 3%:R) _ 1) //. rewrite mul1r mulf_div -mulrDl mulrN -[in x in (_ = x)]opprD. rewrite /inC2 /= -leNgt add0r oppr0 mul0r !addr0 !mul1r. rewrite [x in (0 <= ((x + _) + _))]addrC -[x in (0 <= (x + _))]addrA exprMn -(mulNr b) exprMn sqrrN -mulrDl (expr2 ((a^+2 + b^+2)^-1)) -{3}(mulr1 (a^+2 + b^+2)) -invrM // -mulf_div [x in (0 <= _ + x + _)]mulrC !mulrA (mulrK (x:=(a^+2 + b^+2))) // -[in x in (_ = _ && x)]mulNr -mulrDl -{8}(opprK 1) -(opprD a (- 1)) -mulrA -invrM //. rewrite -(mul1r ( - (a - 1) / (a ^+ 2 + b ^+ 2))) -{8}(@mulrK _ (Num.sqrt 3%:R) _ 1) //. rewrite mul1r mulf_div -mulrDl mulNr oppr_ge0 pmulr_lge0. rewrite pmulr_lle0 ?mulrN //. by rewrite invr_gt0 lt_def -unitfE unitrM H H3 /= mulr_ge0 // ?sqrtr_ge0 // addr_ge0 // sqr_ge0. by rewrite invr_gt0 lt_def -unitfE unitrM H H3 /= mulr_ge0 // ?sqrtr_ge0 // addr_ge0 // sqr_ge0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol mathcomp(complex)