Lemma stnsum_add {m : nat} (f g : ⟦m⟧ → nat) : stnsum (λ i, f i + g i) = stnsum f + stnsum g. 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.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.