proposition: Corollary stnsum_left_le' {m n : nat} (f: ⟦n⟧ -> nat) (r:m≤n) : stnsum (f ∘ stn_left' m n r) ≤ stnsum f.
proof: Proof. intros. assert (s := minusplusnmm n m r). rewrite (natpluscomm (n-m) m) in s. generalize r f; clear r f. rewrite <- s; clear s. set (k := n-m). generalize k; clear k; intros k r f. induction (natpluscomm m k). rewrite stn_left_compare. rewrite stnsum_left_right. apply natlehnplusnm. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions