Lemma partial_sum_prop {n : nat} {m : ⟦n⟧ → nat} {l : nat} : isaprop (∑ (i : ⟦n⟧ ) (j : ⟦m i⟧ ), stnsum (m ∘ stn_left'' (stnlt i)) + j = l). Proof. intros. apply invproofirrelevance. intros t t'. induction t as [i je]. induction je as [j e]. induction t' as [i' je']. induction je' as [j' e']. pose (e'' := e @ !e'). assert (i = i') as p. { induction (nat_eq_or_neq i i') as [eq | ne]. + apply subtypePath_prop. assumption. + apply fromempty. generalize e''. apply nat_neq_to_nopath. induction (natneqchoice _ _ ne); [apply natgthtoneq | apply natlthtoneq]; apply partial_sum_prop_aux; assumption. } apply total2_paths_f with p. - use total2_paths_f. + induction p. simpl. apply subtypePath_prop. apply (natpluslcan _ _ _ e''). + apply isasetnat. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.