proposition: Lemma stnsum_const {m c : nat} : stnsum (λ i: ⟦m⟧, c) = m*c.
proof: Proof. intros. induction m as [|m I]. - apply idpath. - exact (maponpaths (λ i, i+c) I). Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions