Lemma stnsum_dni {n : nat} (f: ⟦S n⟧ -> nat) (j: ⟦S n⟧ ) : stnsum f = stnsum (f ∘ dni j) + f j. Proof. intros. induction j as [j J]. assert (e2 : j + (n - j) = n). { rewrite natpluscomm. apply minusplusnmm. apply natlthsntoleh. exact J. } assert (e : (S j) + (n - j) = S n). { change (S j + (n - j)) with (S (j + (n - j))). apply maponpaths. exact e2. } intermediate_path (stnsum (λ i, f (transportf stn e i))). - apply (transport_stnsum e). - rewrite (stnsum_left_right (S j) (n - j)); unfold funcomp. apply pathsinv0. rewrite (transport_stnsum e2). rewrite (stnsum_left_right j (n-j)); unfold funcomp. rewrite (stnsum_step (λ x, f (transportf stn e _))); unfold funcomp. apply pathsinv0. rewrite natplusassoc. rewrite (natpluscomm (f _)). rewrite <- natplusassoc. apply map_on_two_paths. + apply map_on_two_paths. * apply stnsum_eq; intro i. induction i as [i I]. apply maponpaths. apply subtypePath_prop. induction e. rewrite idpath_transportf. rewrite stn_left_compute. unfold dni,di, stntonat; simpl. induction (natlthorgeh i j) as [R|R]. -- unfold stntonat; simpl; rewrite transport_stn; simpl. induction (natlthorgeh i j) as [a|b]. ++ apply idpath. ++ contradicts R (natlehneggth b). -- unfold stntonat; simpl; rewrite transport_stn; simpl. induction (natlthorgeh i j) as [V|V]. ++ contradicts I (natlehneggth R). ++ apply idpath. * apply stnsum_eq; intro i. induction i as [i I]. apply maponpaths. unfold dni,di, stn_right, stntonat; repeat rewrite transport_stn; simpl. induction (natlthorgeh (j+i) j) as [X|X]. -- contradicts (negnatlthplusnmn j i) X. -- apply subtypePath_prop. simpl. apply idpath. + apply maponpaths. rewrite transport_stn; simpl. apply subtypePath_prop. apply idpath. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.