proposition: Lemma notinC1201_lr_scale (l r : R) : forall (z : C), l != r -> ~~ inC12 0 1 z = ~~ inC12 0 (r - l) ((r - l)%:C * z).
proof: Proof. case=> a b Hlr. rewrite !/inC12. simpc. rewrite /=. rewrite !exprMn !(mulrA (r - l) _ a) !(mulrA (r - l) _ b) -expr2 -(mulrN _ a) -mulrA -(mulrN _ (b / Num.sqrt 3%:R)) -!(mulrDr ((r - l)^+2)) !negb_or -!leNgt. by rewrite !pmulr_rge0 // lt_def sqr_ge0 sqrf_eq0 subr_eq0 eq_sym Hlr. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol mathcomp(complex)