proposition: Lemma degree_mult_imp : forall (p q : FX) m n, degree m p -> degree (m + n) (p[*]q) -> degree n q.
proof: Proof. unfold degree in |- *. intros. rename X into H. rename X0 into H0. elim H. clear H. intros H H1. elim H0. clear H0. intros H0 H2. cut (degree_le n q). intro H3. split. apply mult_cancel_ap_zero_rht with (nth_coeff m p). astepl (nth_coeff (m + n) (p[*]q)). auto. assumption. apply degree_le_mult_imp with p m; auto. unfold degree in |- *. split. auto. assumption. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia