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