proposition: Lemma Rev_mult : forall n1 n2 p1 p2, degree_le n1 p1 -> degree_le n2 p2 -> Rev (n1 + n2) (p1[*]p2) [=] Rev n1 p1[*]Rev n2 p2.
proof: Proof. intros. cut (degree_le (n1 + n2) (p1[*]p2)). intro. cut (p1[*]p2 [=] Sum 0 n2 (fun i2 : nat => Sum 0 n1 (fun i1 : nat => monom (nth_coeff i1 p1[*]nth_coeff i2 p2) (i1 + i2)))). intro. cut (Rev (n1 + n2) (p1[*]p2) [=] Sum 0 n2 (fun i2 : nat => Sum 0 n1 (fun i1 : nat => monom (nth_coeff i1 p1[*]nth_coeff i2 p2) (n1 + n2 - (i1 + i2))))). intro. cut (Rev n1 p1 [=] Sum 0 n1 (fun i1 : nat => monom (nth_coeff i1 p1) (n1 - i1))). intro. cut (Rev n2 p2 [=] Sum 0 n2 (fun i2 : nat => monom (nth_coeff i2 p2) (n2 - i2))). intro. cut (Rev n1 p1[*]Rev n2 p2 [=] Sum 0 n2 (fun i2 : nat => Sum 0 n1 (fun i1 : nat => monom (nth_coeff i1 p1[*]nth_coeff i2 p2) (n1 + n2 - (i1 + i2))))). intro. Step_final (Sum 0 n2 (fun i2 : nat => Sum 0 n1 (fun i1 : nat => monom (nth_coeff i1 p1[*]nth_coeff i2 p2) (n1 + n2 - (i1 + i2))))). astepl (Sum 0 n1 (fun i1 : nat => monom (nth_coeff i1 p1) (n1 - i1)) [*] Sum 0 n2 (fun i2 : nat => monom (nth_coeff i2 p2) (n2 - i2))). apply eq_transitive_unfolded with (Sum 0 n2 (fun i2 : nat => Sum 0 n1 (fun i1 : nat => monom (nth_coeff i1 p1) (n1 - i1)) [*] monom (nth_coeff i2 p2) (n2 - i2))). apply eq_symmetric_unfolded. apply mult_distr_sum_lft with (f := fun i2 : nat => monom (nth_coeff i2 p2) (n2 - i2)). apply Sum_wd'. auto with arith. intro i2. intros. astepl (monom (nth_coeff i2 p2) (n2 - i2) [*] Sum 0 n1 (fun i1 : nat => monom (nth_coeff i1 p1) (n1 - i1))). apply eq_transitive_unfolded with (Sum 0 n1 (fun i1 : nat => monom (nth_coeff i2 p2) (n2 - i2) [*]monom (nth_coeff i1 p1) (n1 - i1))). apply eq_symmetric_unfolded. apply mult_distr_sum_lft with (f := fun i1 : nat => monom (nth_coeff i1 p1) (n1 - i1)). apply Sum_wd'. auto with arith. intro i1. intros. astepl (monom (nth_coeff i1 p1) (n1 - i1) [*]monom (nth_coeff i2 p2) (n2 - i2)). astepl (monom (nth_coeff i1 p1[*]nth_coeff i2 p2) (n1 - i1 + (n2 - i2))). replace (n1 - i1 + (n2 - i2)) with (n1 + n2 - (i1 + i2)). algebra. lia. unfold Rev in |- *. algebra. unfold Rev in |- *. algebra. astepl (Rev (n1 + n2) (Sum 0 n2 (fun i2 : nat => Sum 0 n1 (fun i1 : nat => monom (nth_coeff i1 p1[*]nth_coeff i2 p2) (i1 + i2))))). apply eq_transitive_unfolded with (Sum 0 n2 (fun i2 : nat => Rev (n1 + n2) (Sum 0 n1 (fun i1 : nat => monom (nth_coeff i1 p1[*]nth_coeff i2 p2) (i1 + i2))))). apply Rev_sum with (a_ := fun i2 : nat => Sum 0 n1 (fun i1 : nat => monom (nth_coeff i1 p1[*]nth_coeff i2 p2) (i1 + i2))). apply Sum_wd'. auto with arith. intro i2. intros. apply eq_transitive_unfolded with (Sum 0 n1 (fun i1 : nat => Rev (n1 + n2) (monom (nth_coeff i1 p1[*]nth_coeff i2 p2) (i1 + i2)))). apply Rev_sum with (a_ := fun i1 : nat => monom (nth_coeff i1 p1[*]nth_coeff i2 p2) (i1 + i2)). apply Sum_wd'. auto with arith. intro i1. intros. apply Rev_monom. lia. astepl (Sum 0 n1 (fun i1 : nat => monom (nth_coeff i1 p1) i1) [*] Sum 0 n2 (fun i2 : nat => monom (nth_coeff i2 p2) i2)). apply eq_transitive_unfolded with (Sum 0 n2 (fun i2 : nat => Sum 0 n1 (fun i1 : nat => monom (nth_coeff i1 p1) i1) [*] monom (nth_coeff i2 p2) i2)). apply eq_symmetric_unfolded. apply mult_distr_sum_lft with (f := fun i2 : nat => monom (nth_coeff i2 p2) i2). apply Sum_wd'. auto with arith. intro i2. intros. astepl (monom (nth_coeff i2 p2) i2[*] Sum 0 n1 (fun i1 : nat => monom (nth_coeff i1 p1) i1)). apply eq_transitive_unfolded with (Sum 0 n1 (fun i1 : nat => monom (nth_coeff i2 p2) i2[*]monom (nth_coeff i1 p1) i1)). apply eq_symmetric_unfolded. apply mult_distr_sum_lft with (f := fun i1 : nat => monom (nth_coeff i1 p1) i1). apply Sum_wd'. auto with arith. intro i1. intros. Step_final (monom (nth_coeff i1 p1) i1[*]monom (nth_coeff i2 p2) i2). unfold RX in |- *. apply degree_le_mult; auto. Qed.
imports: CoRN.algebra.CPoly_Degree Coq(Lia)