Lemma stnsum_lt {m : nat} (f g : ⟦m⟧ → nat) : ( ∏ i, f i < g i ) → stnsum g ≥ stnsum f + m. Proof. intros. set (h := λ i, f i + 1). assert (E : stnsum h = stnsum f + m). { unfold h; clear h. rewrite stnsum_add. rewrite stnsum_1. apply idpath. } rewrite <- E. apply stnsum_le. intros i. unfold h. apply natlthtolehp1. apply X. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.