proposition: Theorem lap_convol_mul_cons_succ : ∀ a b lb i len, lap_eq (lap_convol_mul r [a] [b … lb] (S i) len) (lap_convol_mul r [a] lb i len).
proof: Proof. intros a b lb i len. revert a b lb i. induction len; intros; [ reflexivity | idtac ]. constructor; [ idtac | apply IHlen ]. rewrite summation_split_last; [ idtac | apply Nat.le_0_l ]. rewrite List.nth_overflow; [ idtac | simpl; fast_omega ]. rewrite rng_mul_0_l, rng_add_0_r. apply summation_compat; intros j (_, Hj). apply rng_mul_compat_l. rewrite Nat.sub_succ_l; [ reflexivity | assumption ]. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation