proposition: Theorem summation_mul_list_nth_lap_convol_mul : ∀ la lb lc k, (Σ (i = 0, k), List.nth i la 0 * List.nth (k - i) (lap_convol_mul r lb lc 0 (pred (length lb + length lc))) 0 = Σ (i = 0, k), List.nth i la 0 * Σ (j = 0, k - i), List.nth j lb 0 * List.nth (k - i - j) lc 0)%K.
proof: Proof. intros la lb lc k. apply summation_compat; intros i (_, Hi). apply rng_mul_compat_l. rewrite list_nth_lap_convol_mul; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation