Lemma stnsum_left_right (m n : nat) (f: ⟦m+n⟧ -> nat) : stnsum f = stnsum (f ∘ stn_left m n) + stnsum (f ∘ stn_right m n). Proof. intros. induction n as [|n IHn]. { change (stnsum _) with 0 at 3. rewrite natplusr0. assert (e := ! natplusr0 m). rewrite (transport_stnsum e). apply stnsum_eq; intro i. simpl. apply maponpaths. apply pathsinv0. apply stn_left_0. } rewrite stnsum_step. assert (e : S (m+n) = m + S n). { apply pathsinv0. apply natplusnsm. } rewrite (transport_stnsum e). rewrite stnsum_step. rewrite <- natplusassoc. apply map_on_two_paths. { rewrite IHn; clear IHn. apply map_on_two_paths. { apply stnsum_eq; intro i. simpl. apply maponpaths. apply subtypePath_prop. rewrite stn_left_compute. induction e. rewrite idpath_transportf. rewrite dni_last. apply idpath. } { apply stnsum_eq; intro i. simpl. apply maponpaths. apply subtypePath_prop. rewrite stn_right_compute. unfold stntonat. induction e. rewrite idpath_transportf. rewrite 2? dni_last. apply idpath. } } simpl. apply maponpaths. apply subtypePath_prop. induction e. apply idpath. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.