Lemma _c_ {n : nat} {m: ⟦ n ⟧ → nat} (ij : ∑ i : ⟦ n ⟧, ⟦ m i ⟧) : stnsum (m ∘ stn_left'' (stnlt (pr1 ij))) + pr2 ij < stnsum m. Proof. intros. set (m1 := m ∘ stn_left'' (stnlt (pr1 ij))). induction ij as [i j]. induction i as [i I]. induction j as [j J]. simpl in m1. change (stnsum m1 + j < stnsum m). assert (s := stnsum_left_le' m (I : S i ≤ n)). use (natlthlehtrans _ _ _ _ s). clear s. induction n as [|n _]. - induction (negnatlthn0 _ I). - assert (t : stnsum m1 + j < stnsum m1 + m (i,,I)). { apply natlthandplusl. exact J. } apply (natlthlehtrans _ _ _ t). assert (K : ∏ m n, m = n -> m ≤ n). { intros a b e. induction e. apply isreflnatleh. } apply K; clear K. rewrite stnsum_step. clear j J t. unfold m1 ; clear m1. apply two_arg_paths. + apply stnsum_eq. intro l. simpl. apply maponpaths. apply subtypePath_prop; simpl. apply pathsinv0, di_eq1, stnlt. + simpl. apply maponpaths. apply subtypePath_prop. simpl. apply idpath. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.