Corollary stnsum_left_le' {m n : nat} (f: ⟦n⟧ -> nat) (r:m≤n) : stnsum (f ∘ stn_left' m n r) ≤ stnsum f. 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.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.