Lemma iterop_fun_nat {n:nat} (x:stn n->nat) : iterop_fun 0 add x = stnsum x. Proof. intros. induction n as [|n I]. - reflexivity. - induction n as [|n _]. + reflexivity. + simple refine (iterop_fun_step 0 add natplusl0 _ @ _ @ ! stnsum_step _). apply (maponpaths (λ i, i + x lastelement)). apply I. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.NegativePropositions.