proposition: Theorem lap_convol_mul_lap_add : ∀ la lb lc i len, lap_eq (lap_convol_mul r la (lap_add lb 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 ]. apply summation_compat; intros j (_, Hj). apply rng_mul_compat_l. rewrite list_nth_add; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation