proposition: Lemma Shift_degree_le : forall a p n, degree_le n p -> degree_le n (Shift a p).
proof: Proof. intros. unfold Shift in |- *. apply Sum_degree_le. auto with arith. intros. elim (le_lt_dec i n); intros. replace n with (0 + n). 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. unfold degree_le in H. apply degree_le_wd with (_C_ ([0]:CC)). astepl ([0]:cpoly_cring CC). astepl ([0][*] (_X_[+]_C_ a) [^]i). apply bin_op_wd_unfolded. Step_final (_C_ ([0]:CC)). algebra. apply degree_le_mon with 0. auto with arith. apply degree_le_c_. Qed.
imports: CoRN.complex.CComplex Coq(Lia)