proposition: Lemma stnsum_first_le {n : nat} (f: ⟦S n⟧ -> nat) : f firstelement ≤ stnsum f.
proof: 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.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions