proposition: Lemma Shift_shift : forall a p, Shift [--]a (Shift a p) [=] p.
proof: Proof. intros. apply poly_CC_extensional. intros. astepl (Shift a p) ! (x[+][--]a). astepl p ! (x[+][--]a[+]a). apply apply_wd. algebra. rational. Qed.
imports: CoRN.complex.CComplex Coq(Lia)