proposition: Theorem summation_mul_list_nth_lap_convol_mul_2 : ∀ la lb lc k, (Σ (i = 0, k), List.nth i lc 0 * List.nth (k - i) (lap_convol_mul r la lb 0 (pred (length la + length lb))) 0 = Σ (i = 0, k), List.nth (k - i) lc 0 * Σ (j = 0, i), List.nth j la 0 * List.nth (i - j) lb 0)%K.
proof: Proof. intros la lb lc k. rewrite summation_rtl. apply summation_compat; intros i (_, Hi). rewrite Nat.add_0_r. apply rng_mul_compat_l. rewrite Nat_sub_sub_distr; [ idtac | assumption ]. rewrite Nat.add_comm, Nat.add_sub. apply list_nth_lap_convol_mul; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation