{A : AbGroup} (n : nat) (f g : forall k, (k < n)%nat -> A) : ab_sum n (fun k Hk => f k Hk + g k Hk) = ab_sum n (fun k Hk => f k Hk) + ab_sum n (fun k Hk => g k Hk). Proof. induction n as [|n IHn]. 1: by rewrite grp_unit_l. simpl. rewrite <- !grp_assoc; f_ap. rewrite IHn, ab_comm, <- grp_assoc; f_ap. by rewrite ab_comm. Defined.
Require Import Basics.Overture Basics.Tactics. Require Import Spaces.Nat.Core Spaces.Int. Require Import AbelianGroup.