proposition: Theorem series_mul_assoc : ∀ a b c, (a * (b * c) = (a * b) * c)%ser.
proof: Proof. intros a b c. constructor; intros k; simpl. unfold convol_mul; simpl. unfold convol_mul; simpl. symmetry. rewrite summation_mul_comm. 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 NbarM Field2 Fsummation