Lemma stnsum_ge1 {m : nat} (f : ⟦m⟧ → nat) : ( ∏ i, f i ≥ 1 ) → stnsum f ≥ m. Proof. intros G. set (g := λ i:⟦m⟧, 1). assert (E : stnsum g = m). { apply stnsum_1. } assert (F : stnsum g ≤ stnsum f). { apply stnsum_le. exact G. } generalize E F; generalize (stnsum g); clear E F g; intros s e i. induction e. exact i. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.