Lemma stnsum_first_le {n : nat} (f: ⟦S n⟧ -> nat) : f firstelement ≤ stnsum f. Proof. intros. induction n as [|n IH]. - apply isreflnatleh. - rewrite stnsum_step. assert (W := IH (f ∘ dni lastelement)). change ((f ∘ dni lastelement) firstelement) with (f firstelement) in W. apply (istransnatleh W); clear W. apply natlehnplusnm. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.