proposition: Lemma degree_le_mult : forall (p q : RX) m n, degree_le m p -> degree_le n q -> degree_le (m + n) (p[*]q).
proof: Proof. unfold degree_le in |- *. intros. astepl (Sum 0 m0 (fun i : nat => nth_coeff i p[*]nth_coeff (m0 - i) q)). apply Sum_zero. auto with arith. intros. cut ({m < i} + {n < m0 - i}). intro. elim H4; clear H4; intros. Step_final ([0][*]nth_coeff (m0 - i) q). Step_final (nth_coeff i p[*][0]). elim (lt_eq_lt_dec m i); intro. elim a; intro. auto. right. lia. right. lia. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia