proposition: Theorem list_nth_lap_mul : ∀ la lb k, (List.nth k (lap_mul la lb) 0 = Σ (i = 0, k), List.nth i la 0 * List.nth (k - i) lb 0)%K.
proof: Proof. intros la lb k. apply list_nth_convol_mul; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation