Lemma stnsum_diffs {m : nat} (f : ⟦S m⟧ → nat) : is_stn_increasing f -> stnsum (λ i, f (dni_firstelement i) - f (dni_lastelement i)) = f lastelement - f firstelement. Proof. intros e. induction m as [|m I]. - change (0 = f firstelement - f firstelement). apply pathsinv0. apply minuseq0'. - rewrite stnsum_step. change (f (dni_firstelement lastelement)) with (f lastelement). rewrite natpluscomm. use (_ @ ! @natdiffplusdiff (f lastelement) (f (dni_lastelement lastelement)) (f firstelement) _ _). + apply maponpaths. use (_ @ I (f ∘ dni_lastelement) _ @ _). * simpl. apply stnsum_eq; intros i. rewrite replace_dni_last. apply idpath. * intros i j s. unfold funcomp. apply e. apply s. * apply idpath. + apply e. apply lastelement_ge. + apply e. apply firstelement_le. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.