{A : AbGroup} (n : nat) (a : A) (f : forall k, (k < n)%nat -> A) (p : forall k Hk, f k Hk = a) : ab_sum n f = ab_mul n a. Proof. induction n as [|n IHn] in f, p |- *. - reflexivity. - rhs_V nrapply (ap@{Set _} _ (int_nat_succ n)). rhs nrapply grp_pow_succ. simpl. f_ap. apply IHn. intros. apply p. Defined.
Require Import Basics.Overture Basics.Tactics. Require Import Spaces.Nat.Core Spaces.Int. Require Import AbelianGroup.