{R : Ring} (n : nat) (f : forall k, (k < n)%nat -> R) (r : R) : r * ab_sum n f = ab_sum n (fun k Hk => r * f k Hk). Proof. induction n as [|n IHn]. 1: apply rng_mult_zero_r. lhs nrapply rng_dist_l; 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.