proposition: Lemma Shift_mult : forall a p1 p2, Shift a (p1[*]p2) [=] Shift a p1[*]Shift a p2.
proof: Proof. intros. apply poly_CC_extensional. intros. astepl (p1[*]p2) ! (x[+]a). astepl (p1 ! (x[+]a) [*]p2 ! (x[+]a)). Step_final ((Shift a p1) ! x[*] (Shift a p2) ! x). Qed.
imports: CoRN.complex.CComplex Coq(Lia)