proposition: Theorem lap_mul_cons_l : ∀ a la lb, lap_eq (lap_mul [a … la] lb) (lap_add (lap_mul [a] lb) [0%K … lap_mul la lb]).
proof: Proof. intros a la lb. unfold lap_mul. apply list_nth_lap_eq; intros k. rewrite list_nth_lap_convol_mul; [ idtac | reflexivity ]. rewrite list_nth_add. rewrite list_nth_lap_convol_mul; [ idtac | reflexivity ]. destruct k. rewrite summation_only_one. rewrite summation_only_one. rewrite rng_add_0_r; reflexivity. rewrite summation_split_first; [ idtac | apply Nat.le_0_l ]. rewrite Nat.sub_0_r. symmetry. rewrite summation_split_first; [ idtac | apply Nat.le_0_l ]. rewrite all_0_summation_0. rewrite Nat.sub_0_r. simpl. rewrite rng_add_0_r. apply rng_add_compat_l. rewrite list_nth_lap_convol_mul; [ idtac | reflexivity ]. rewrite summation_succ_succ; reflexivity. intros i (Hi, Hik); simpl. destruct i; [ exfalso; fast_omega Hi | simpl ]. destruct i; rewrite rng_mul_0_l; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation