proposition: Theorem lap_convol_mul_nil_l : ∀ α (R : ring α) l i len, lap_eq (lap_convol_mul R [] l i len) [].
proof: Proof. intros α R l i len. revert i. induction len; intros; [ reflexivity | simpl ]. constructor; [ idtac | apply IHlen ]. rewrite all_0_summation_0; [ reflexivity | idtac ]. intros k (_, Hk). destruct k; rewrite rng_mul_0_l; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation