Lemma stnsum_pos {n : nat} (f: ⟦n⟧ -> nat) (j: ⟦n⟧ ) : f j ≤ stnsum f. Proof. assert (m : 0 < n). { apply (natlehlthtrans _ j). - apply natleh0n. - exact (pr2 j). } assert (l : 1 ≤ n). { apply natlthtolehsn. assumption. } assert (e : n = S (n - 1)). { change (S (n - 1)) with (1 + (n - 1)). rewrite natpluscomm. apply pathsinv0. apply minusplusnmm. assumption. } rewrite (transport_stnsum (!e) f). rewrite (stnsum_dni _ (transportf stn e j)). unfold funcomp. generalize (stnsum (λ x, f (transportf stn (! e) (dni (transportf stn e j) x)))); intro s. induction e. apply natlehmplusnm. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.