{A : AbGroup} (n : nat) (f : forall k, (k < n)%nat -> A) (p : forall k Hk, f k Hk = 0) : ab_sum n f = 0. Proof. lhs nrapply (ab_sum_const _ 0 f p). apply grp_pow_unit. Defined.
Require Import Basics.Overture Basics.Tactics. Require Import Spaces.Nat.Core Spaces.Int. Require Import AbelianGroup.