proposition: Lemma degree_mult_aux : forall (p q : RX) m n, degree_le m p -> degree_le n q -> nth_coeff (m + n) (p[*]q) [=] nth_coeff m p[*]nth_coeff n q.
proof: Proof. unfold degree_le in |- *. intros. astepl (Sum 0 (m + n) (fun i : nat => nth_coeff i p[*]nth_coeff (m + n - i) q)). astepl (Sum 0 m (fun i : nat => nth_coeff i p[*]nth_coeff (m + n - i) q) [+] Sum (S m) (m + n) (fun i : nat => nth_coeff i p[*]nth_coeff (m + n - i) q)). astepr (nth_coeff m p[*]nth_coeff n q[+][0]). apply bin_op_wd_unfolded. elim (O_or_S m); intro y. elim y. clear y. intros x y. rewrite <- y in H. rewrite <- y. apply eq_transitive_unfolded with (Sum 0 x (fun i : nat => nth_coeff i p[*]nth_coeff (S x + n - i) q) [+] nth_coeff (S x) p[*]nth_coeff (S x + n - S x) q). apply Sum_last with (f := fun i : nat => nth_coeff i p[*]nth_coeff (S x + n - i) q). astepr ([0][+]nth_coeff (S x) p[*]nth_coeff n q). apply bin_op_wd_unfolded. apply Sum_zero. auto with arith. intros. cut (n < S x + n - i). intro. Step_final (nth_coeff i p[*][0]). lia. replace (S x + n - S x) with n. algebra. auto with arith. rewrite <- y in H. rewrite <- y. pattern n at 2 in |- *. replace n with (0 + n - 0). apply Sum_one with (f := fun i : nat => nth_coeff i p[*]nth_coeff (0 + n - i) q). auto with arith. apply Sum_zero. auto with arith. intros. cut (m < i). intro. Step_final ([0][*]nth_coeff (m + n - i) q). auto. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia