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