proposition: Lemma stnsum_lt {m : nat} (f g : ⟦m⟧ → nat) : ( ∏ i, f i < g i ) → stnsum g ≥ stnsum f + m.
proof: 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.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions