proposition: Lemma degree_le_mult_imp : forall (p q : FX) m n, degree m p -> degree_le (m + n) (p[*]q) -> degree_le n q.
proof: Proof. unfold degree in |- *. unfold degree_le in |- *. intros. rename H0 into H1. rename H into H0. rename X into H. elim H. clear H. intros H2 H3. elim (Cpoly_ex_degree _ q). unfold degree_le in |- *. intro N. intro H4. cut (forall k i : nat, n < i -> N - k < i -> nth_coeff i q [=] [0]). intro H5. elim (le_lt_dec m0 N); intros H6. replace m0 with (N - (N - m0)). apply H5 with (N - n). lia. lia. lia. apply H4; auto. intro. induction k as [| k Hreck]; intros. apply H4. rewrite Nat.sub_0_r in H5; auto. elim (le_lt_eq_dec (N - k) i); try intro y. auto. rewrite y in Hreck. apply mult_cancel_lft with (nth_coeff m p). auto. astepr ([0]:F). apply eq_transitive_unfolded with (Sum 0 (m + i) (fun j : nat => nth_coeff j p[*]nth_coeff (m + i - j) q)). pattern i at 1 in |- *. replace i with (m + i - m). apply eq_symmetric_unfolded. apply Sum_term with (f := fun j : nat => nth_coeff j p[*]nth_coeff (m + i - j) q). auto with arith. auto with arith. intros. elim (le_lt_dec j m); intros. cut (i < m + i - j). intro. cut (n < m + i - j). intro. Step_final (nth_coeff j p[*][0]). lia. lia. Step_final ([0][*]nth_coeff (m + i - j) q). auto with arith. astepl (nth_coeff (m + i) (p[*]q)). cut (m + n < m + i). intro. auto. auto with arith. lia. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia