{A : AbGroup} {n : nat} {f g : forall k, (k < n)%nat -> A} (p : forall k Hk, f k Hk = g k Hk) : ab_sum n f = ab_sum n g. Proof. induction n as [|n IHn]. 1: reflexivity. cbn; f_ap. by apply IHn. Defined.
Require Import Basics.Overture Basics.Tactics. Require Import Spaces.Nat.Core Spaces.Int. Require Import AbelianGroup.