proposition: Lemma stnsum_le {n : nat} (f g: ⟦n⟧ -> nat) : (∏ i, f i ≤ g i) -> stnsum f ≤ stnsum g.
proof: Proof. intros le. induction n as [|n IH]. - simpl. apply idpath. - apply natlehandplus. + apply IH. intro i. apply le. + apply le. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions