Lemma stnsum_last_le {n : nat} (f: ⟦S n⟧ -> nat) : f lastelement ≤ stnsum f. Proof. intros. rewrite stnsum_step. apply natlehmplusnm. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.