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