proposition: Theorem lap_convol_mul_succ : ∀ α (r : ring α) la lb i len, lap_eq (lap_convol_mul r la lb i (S len)) (lap_convol_mul r la lb i len ++ [Σ (j = 0, i + len), List.nth j la 0 * List.nth (i + len - j) lb 0])%K.
proof: Proof. intros α r la lb i len. revert la lb i. induction len; intros; simpl. rewrite Nat.add_0_r; reflexivity. constructor; [ reflexivity | idtac ]. simpl in IHlen. rewrite IHlen. rewrite Nat.add_succ_r, Nat.add_succ_l. reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation