proposition: Theorem list_nth_lap_convol_mul : ∀ la lb i len, len = pred (length la + length lb) → (List.nth i (lap_convol_mul r la lb 0 len) 0 = Σ (j = 0, i), List.nth j la 0 * List.nth (i - j) lb 0)%K.
proof: Proof. intros la lb i len Hlen. symmetry in Hlen. rewrite list_nth_lap_convol_mul_aux; [ idtac | assumption ]. rewrite Nat.add_0_r; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation