proposition: Theorem list_nth_convol_mul : ∀ la lb i k len, (i + len)%nat = pred (length la + length lb) → (List.nth k (lap_convol_mul r la lb i len) 0 = Σ (j = 0, i + k), List.nth j la 0 * List.nth (i + k - j) lb 0)%K.
proof: Proof. intros la lb i k len Hilen. revert la lb i k Hilen. induction len; intros; simpl. rewrite match_id; simpl. rewrite all_0_summation_0; [ reflexivity | simpl ]. intros j (_, Hj). destruct (lt_dec j (length la)) as [Hja| Hja]. destruct (lt_dec (i + k - j) (length lb)) as [Hjb| Hjb]. exfalso; fast_omega Hilen Hja Hjb. apply rng_mul_eq_0; right. apply Nat.nlt_ge in Hjb. rewrite List.nth_overflow; [ reflexivity | assumption ]. apply rng_mul_eq_0; left. apply Nat.nlt_ge in Hja. rewrite List.nth_overflow; [ reflexivity | assumption ]. destruct k; [ rewrite Nat.add_0_r; reflexivity | idtac ]. rewrite Nat.add_succ_r, <- Nat.add_succ_l in Hilen. rewrite Nat.add_succ_r, <- Nat.add_succ_l. apply IHlen; assumption. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation