proposition: Theorem lap_mul_cons : ∀ a b la lb, lap_eq (lap_mul [a … la] [b … lb]) [(a * b)%K … lap_add (lap_add (lap_mul la [b]) (lap_mul [a] lb)) [0%K … lap_mul la lb]].
proof: Proof. intros a b la lb. rewrite lap_mul_cons_l; simpl. rewrite summation_only_one. rewrite rng_add_0_r. constructor; [ reflexivity | idtac ]. rewrite lap_mul_cons_r. unfold lap_mul; simpl. rewrite lap_add_assoc. apply lap_add_compat; [ idtac | reflexivity ]. rewrite lap_add_comm. apply lap_add_compat; [ reflexivity | idtac ]. apply lap_convol_mul_cons_succ. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation