proposition: Lemma Shift_apply : forall a p (x : CC), (Shift a p) ! x [=] p ! (x[+]a).
proof: Proof. intros. unfold Shift in |- *. apply eq_transitive_unfolded with (Sum 0 (lth_of_poly p) (fun i : nat => (_C_ (nth_coeff i p) [*] (_X_[+]_C_ a) [^]i) ! x)). apply Sum_cpoly_ap with (f := fun i : nat => _C_ (nth_coeff i p) [*] (_X_[+]_C_ a) [^]i). apply eq_symmetric_unfolded. astepl (Sum 0 (lth_of_poly p) (fun i : nat => _C_ (nth_coeff i p) [*]_X_[^]i)) ! (x[+]a). apply eq_transitive_unfolded with (Sum 0 (lth_of_poly p) (fun i : nat => (_C_ (nth_coeff i p) [*]_X_[^]i) ! (x[+]a))). apply Sum_cpoly_ap with (f := fun i : nat => _C_ (nth_coeff i p) [*]_X_[^]i). apply Sum_wd. intros. astepl ((_C_ (nth_coeff i p)) ! (x[+]a) [*] (_X_[^]i) ! (x[+]a)). astepl (nth_coeff i p[*]_X_ ! (x[+]a) [^]i). astepl (nth_coeff i p[*] (x[+]a) [^]i). astepl (nth_coeff i p[*] (_X_ ! x[+] (_C_ a) ! x) [^]i). astepl (nth_coeff i p[*] (_X_[+]_C_ a) ! x[^]i). Step_final ((_C_ (nth_coeff i p)) ! x[*] ((_X_[+]_C_ a) [^]i) ! x). Qed.
imports: CoRN.complex.CComplex Coq(Lia)