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