proposition: Lemma stnsum_add {m : nat} (f g : ⟦m⟧ → nat) : stnsum (λ i, f i + g i) = stnsum f + stnsum g.
proof: Proof. intros. induction m as [|m I]. - apply idpath. - rewrite 3 stnsum_step. change ((λ i : ⟦ S m ⟧, f i + g i) ∘ dni lastelement) with (λ y : ⟦ m ⟧, f (dni lastelement y) + g (dni lastelement y)). rewrite I. rewrite natplusassoc. rewrite natplusassoc. simpl. apply maponpaths. rewrite natpluscomm. rewrite natplusassoc. apply maponpaths. rewrite natpluscomm. apply idpath. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions