Definition finsum' {X} (fin : isfinite X) (f : X → nat) : nat. Proof. intros. exact (fincard (isfinitetotal2 (stn∘f) fin (λ i, isfinitestn (f i)))). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.NegativePropositions.