proposition: Theorem convol_mul_comm : ∀ a b i, (convol_mul a b i = convol_mul b a i)%K.
proof: Proof. intros a b k. unfold convol_mul. rewrite summation_rtl. apply summation_compat; intros i Hi. rewrite Nat.add_0_r. rewrite Nat_sub_sub_distr; [ idtac | destruct Hi; auto ]. rewrite Nat.add_comm, Nat.add_sub, rng_mul_comm; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation