{R : Ring} (M : LeftModule R) (n : nat) (f : forall k, (k < n)%nat -> R) (x : M) : ab_sum n f *L x = ab_sum n (fun k Hk => f k Hk *L x). Proof. induction n as [|n IHn]. 1: apply lm_zero_l. lhs nrapply lm_dist_r; simpl; f_ap. Defined.
Require Import WildCat. Require Import Spaces.Nat.Core. Require Import Classes.interfaces.canonical_names. Require Import Algebra.Groups.Kernel Algebra.Groups.Image Algebra.Groups.QuotientGroup. Require Import Algebra.AbGroups.AbelianGroup Algebra.AbGroups.Biproduct. Require Import Rings.Ring.