{A : AbGroup} (n : nat) (f : forall k, (k < n)%nat -> A) : A. Proof. induction n as [|n IHn]. - exact zero. - refine (f n _ + IHn _). intros k Hk. exact (f k _). Defined.
Require Import Basics.Overture Basics.Tactics. Require Import Spaces.Nat.Core Spaces.Int. Require Import AbelianGroup.