proposition: Theorem lap_convol_mul_comm : ∀ α (R : ring α) l₁ l₂ i len, lap_eq (lap_convol_mul R l₁ l₂ i len) (lap_convol_mul R l₂ l₁ i len).
proof: Proof. intros α R l₁ l₂ i len. revert i. induction len; intros; [ reflexivity | simpl ]. constructor; [ idtac | apply IHlen ]. rewrite summation_rtl. apply summation_compat; intros j (_, Hj). rewrite Nat.add_0_r. rewrite rng_mul_comm. apply rng_mul_compat; [ idtac | reflexivity ]. rewrite Nat_sub_sub_distr; [ idtac | assumption ]. rewrite Nat.add_comm, Nat.add_sub; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation