proposition: Theorem lap_mul_assoc : ∀ la lb lc, lap_eq (lap_mul la (lap_mul lb lc)) (lap_mul (lap_mul la lb) lc).
proof: Proof. intros la lb lc. symmetry; rewrite lap_mul_comm. unfold lap_mul. apply list_nth_lap_eq; intros k. rewrite list_nth_lap_convol_mul; [ idtac | reflexivity ]. rewrite list_nth_lap_convol_mul; [ idtac | reflexivity ]. rewrite summation_mul_list_nth_lap_convol_mul_2; symmetry. rewrite summation_mul_list_nth_lap_convol_mul; symmetry. rewrite <- summation_summation_mul_swap. rewrite <- summation_summation_mul_swap. rewrite summation_summation_exch. rewrite summation_summation_shift. apply summation_compat; intros i Hi. apply summation_compat; intros j Hj. rewrite rng_mul_comm, rng_mul_assoc. rewrite Nat.add_comm, Nat.add_sub. rewrite Nat.add_comm, Nat.sub_add_distr. reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation