proposition: Theorem lap_add_lap_convol_mul : ∀ la lb lc i len, lap_eq (lap_add (lap_convol_mul r la lb i len) (lap_convol_mul r la lc i len)) (lap_convol_mul_add la lb lc i len).
proof: Proof. intros la lb lc i len. revert la lb lc i. induction len; intros; [ reflexivity | simpl ]. constructor; [ idtac | apply IHlen ]. rewrite <- summation_add_distr. apply summation_compat; intros j (_, Hj). rewrite rng_mul_add_distr_l; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation