Lemma partial_sum_slot {n : nat} {m : ⟦n⟧ → nat} {l : nat} : l < stnsum m -> ∃! (i : ⟦n⟧ ) (j : ⟦m i⟧ ), stnsum (m ∘ stn_left'' (stnlt i)) + j = l. Proof. intros lt. set (len := stnsum m). induction n as [|n IH]. { apply fromempty. change (hProptoType(l < 0)) in lt. exact (negnatlthn0 _ lt). } set (m' := m ∘ dni_lastelement). set (len' := stnsum m'). induction (natlthorgeh l len') as [I|J]. - assert (IH' := IH m' I); clear IH. induction IH' as [ijJ Q]. induction ijJ as [i jJ]. induction jJ as [j J]. use tpair. + exists (dni_lastelement i). exists j. abstract (use (_ @ J); apply (maponpaths (λ x, x+j)); apply stnsum_eq; intro r; unfold m'; simpl; apply maponpaths; apply subtypePath_prop, idpath). + intro t. apply partial_sum_prop. - clear IH. set (j := l - len'). apply iscontraprop1. { apply partial_sum_prop. } assert (K := minusplusnmm _ _ J). change (l-len') with j in K. exists lastelement. use tpair. * exists j. apply (natlthandpluslinv _ _ len'). rewrite natpluscomm. induction (!K); clear K J j. assert(C : len = len' + m lastelement). { use (stnsum_step _ @ _). unfold len', m'; clear m' len'. rewrite replace_dni_last. apply idpath. } induction C. exact lt. * simpl. intermediate_path (stnsum m' + j). -- apply (maponpaths (λ x, x+j)). apply stnsum_eq; intro i. unfold m'. simpl. apply maponpaths. apply subtypePath_prop, idpath. -- rewrite natpluscomm. exact K. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.