proposition: Corollary stnsum_left_le (m n : nat) (f: ⟦m+n⟧ -> nat) : stnsum (f ∘ stn_left m n) ≤ stnsum f.
proof: Proof. intros. rewrite stnsum_left_right. apply natlehnplusnm. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions