{R : Ring} (n : nat) (f : forall k, (k < n)%nat -> R) (r : R) : ab_sum n f * r = ab_sum n (fun k Hk => f k Hk * r). Proof. induction n as [|n IHn]. 1: apply rng_mult_zero_l. lhs nrapply rng_dist_r; simpl; f_ap. Defined.
Require Import WildCat. Require Import Spaces.Nat.Core Spaces.Nat.Arithmetic. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.Groups.Group Algebra.Groups.Subgroup. Require Import Modalities.ReflectiveSubuniverse.