proposition: Lemma iterop_fun_nat {n:nat} (x:stn n->nat) : iterop_fun 0 add x = stnsum x.
proof: 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.
imports: UniMath.Combinatorics.Lists UniMath.Combinatorics.FiniteSequences UniMath.Algebra.RigsAndRings UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.Algebra.Groups UniMath.MoreFoundations.NegativePropositions UniMath.Combinatorics.FiniteSets UniMath.Foundations.NaturalNumbers