proposition: Lemma Shift_monic : forall a p n, monic n p -> monic n (Shift a p).
proof: Proof. intros. unfold monic in H. elim H. clear H. intros H H0. unfold degree_le in H0. apply monic_wd with (Sum 0 n (fun i : nat => _C_ (nth_coeff i p) [*] (_X_[+]_C_ a) [^]i)). astepl (Sum 0 n (fun i : nat => _C_ (nth_coeff i p) [*] (_X_[+]_C_ a) [^]i) [+][0]). apply eq_transitive_unfolded with (Sum 0 n (fun i : nat => _C_ (nth_coeff i p) [*] (_X_[+]_C_ a) [^]i) [+] Sum (S n) (lth_of_poly p) (fun i : nat => _C_ (nth_coeff i p) [*] (_X_[+]_C_ a) [^]i)). apply bin_op_wd_unfolded. algebra. apply eq_symmetric_unfolded. apply Sum_zero. cut (n < lth_of_poly p). intro. auto with arith. apply lt_i_lth_of_poly. astepl ([1]:CC). algebra. intros. cut (n < i). intro. astepl (_C_ [0][*] (_X_[+]_C_ a) [^]i). Step_final ([0][*] (_X_[+]_C_ a) [^]i). auto with arith. unfold Shift in |- *. apply Sum_Sum. elim (O_or_S n); intro y. elim y. clear y. intros x y. rewrite <- y in H. rewrite <- y in H0. rewrite <- y. apply monic_wd with (Sum 0 x (fun i : nat => _C_ (nth_coeff i p) [*] (_X_[+]_C_ a) [^]i) [+] (_X_[+]_C_ a) [^]S x). apply eq_transitive_unfolded with (Sum 0 x (fun i : nat => _C_ (nth_coeff i p) [*] (_X_[+]_C_ a) [^]i) [+] _C_ (nth_coeff (S x) p) [*] (_X_[+]_C_ a) [^]S x). apply bin_op_wd_unfolded. algebra. astepl ([1][*] (_X_[+]_C_ a) [^]S x). apply bin_op_wd_unfolded. Step_final (_C_ ([1]:CC)). algebra. apply eq_symmetric_unfolded. apply Sum_last with (f := fun i : nat => _C_ (nth_coeff i p) [*] (_X_[+]_C_ a) [^]i). apply monic_plus with x. apply Sum_degree_le. auto with arith. intros. replace x with (0 + x). apply degree_le_mult. apply degree_le_c_. apply degree_le_mon with (1 * i). lia. apply degree_le_nexp. apply degree_imp_degree_le. apply degree_wd with (_C_ a[+]_X_). algebra. apply degree_plus_rht with 0. apply degree_le_c_. apply degree_x_. auto. auto. pattern (S x) at 1 in |- *. replace (S x) with (1 * S x). apply monic_nexp. apply monic_wd with (_C_ a[+]_X_). algebra. apply monic_plus with 0. apply degree_le_c_. apply monic_x_. auto. auto with arith. auto. rewrite <- y in H. rewrite <- y in H0. rewrite <- y. apply monic_wd with ([1]:CCX). unfold Sum in |- *. unfold Sum1 in |- *. simpl in |- *. split. cut ([1] [=] nth_coeff 0 p[*][1][+][0]). auto. astepl (nth_coeff 0 p). rational. auto. apply monic_wd with (_C_ ([1]:CC)). algebra. apply monic_c_one. Qed.
imports: CoRN.complex.CComplex Coq(Lia)