proposition: Theorem lap_convol_mul_nil_r : ∀ α (R : ring α) l i len, lap_eq (lap_convol_mul R l [] i len) [].
proof: Proof. intros α R l i len. rewrite lap_convol_mul_comm. apply lap_convol_mul_nil_l. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation