{R : Ring} (n i : nat) (Hi : (i < n)%nat) (f : forall k, (k < n)%nat -> R) : ab_sum n (fun j Hj => f j Hj * kronecker_delta i j) = f i Hi. Proof. lhs nrapply path_ab_sum. 2: nrapply rng_sum_kronecker_delta_l. intros k Hk. apply kronecker_delta_comm. Defined.
Require Import Basics.Overture Basics.Decidable Spaces.Nat. Require Import Algebra.Rings.Ring. Require Import Classes.interfaces.abstract_algebra.