{R : Ring} (n i : nat) (Hi : (i < n)%nat) (f : forall k, (k < n)%nat -> R) : ab_sum n (fun j Hj => kronecker_delta i j * f j Hj) = f i Hi. Proof. revert i Hi f; simple_induction n n IHn; intros i Hi f. 1: destruct (not_lt_zero_r _ Hi). destruct (dec (i = n)) as [p|p]. - destruct p; simpl. rewrite kronecker_delta_refl. rewrite rng_mult_one_l. rewrite <- rng_plus_zero_r. apply ap11. { apply (ap (fun h => plus (f i h))), path_ishprop. } nrapply ab_sum_zero. intros k Hk. rewrite (kronecker_delta_gt Hk). apply rng_mult_zero_l. - simpl; lhs nrapply ap. + nrapply IHn. apply neq_iff_lt_or_gt in p. destruct p; [assumption|]. apply gt_iff_not_leq in Hi. contradiction Hi. + rewrite (kronecker_delta_neq p). rewrite rng_mult_zero_l. rewrite grp_unit_l. apply ap, path_ishprop. Defined.
Require Import Basics.Overture Basics.Decidable Spaces.Nat. Require Import Algebra.Rings.Ring. Require Import Classes.interfaces.abstract_algebra.