Lemma partial_sum_prop_aux {n : nat} {m : ⟦n⟧ → nat} : ∏ (i i' : ⟦ n ⟧) (j : ⟦ m i ⟧) (j' : ⟦ m i' ⟧), i < i' → stnsum (m ∘ stn_left'' (stnlt i)) + j < stnsum (m ∘ stn_left'' (stnlt i')) + j'. Proof. intros ? ? ? ? lt. apply natlthtolehsn in lt. pose (ltS := (natlehlthtrans _ _ _ lt (stnlt i'))). refine (natlthlehtrans _ _ _ _ (natlehnplusnm _ _)). apply natlthlehtrans with (stnsum (m ∘ stn_left'' ltS)). - rewrite stnsum_step. assert (stnsum (m ∘ stn_left'' (stnlt i)) = stnsum (m ∘ stn_left'' ltS ∘ dni lastelement)) as e. { apply stnsum_eq. intros k. simpl. apply maponpaths. apply subtypePath_prop. simpl. apply pathsinv0, di_eq1. apply (stnlt k). } induction e. apply natlthandplusl. assert ((m ∘ stn_left'' ltS) lastelement = m i) as e. { simpl. apply maponpaths. apply subtypePath_prop, idpath. } induction e. apply (stnlt j). - assert (stnsum (m ∘ stn_left'' ltS) = stnsum (m ∘ stn_left'' (stnlt i') ∘ stn_left' _ _ lt)) as e. { apply stnsum_eq. intros k. simpl. apply maponpaths. apply subtypePath_prop, idpath. } rewrite e. apply stnsum_left_le'. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.