proposition: Lemma stnsum_step {n : nat} (f: ⟦S n⟧ -> nat) : stnsum f = stnsum (f ∘ (dni lastelement)) + f lastelement.
proof: Proof. intros. apply idpath. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions