proposition: Lemma notinC12lr_shift (l r : R) : forall (z : C), l != r -> ~~ inC12 0 (r - l) z = ~~ inC12 l r (z + l%:C).
proof: Proof. case=> a b Hlr. rewrite !/inC12. simpc. rewrite /= !negb_or -!leNgt. by rewrite (expr2 (a+l)) (mulrDl a l) !mulrDr (mulrDl l r) (mulrDl l r) -!expr2 !opprD [l * a + _]addrC !addrA addrK -(addrA _ (- (r * a)) _) (addrC (- (r * a)) _) !addrA addrK -(addrA _ (a * l) _) (addrC (a * l)) (mulrC a l) -{5 9}(opprK l) mulNr -opprD -mulrDl [X in (_ = (0 <= X) && _)]addrC [X in (_ = _ && (0 <= X))]addrC !addrA (addrC (l * r)) -(addrA _ (l * r) _) (addrC (l * r)) (mulrC l r) !addrA addrK. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol mathcomp(complex)