proposition: Lemma vecsum_left_right : ∏ (m n : nat) (f : (⟦ m + n ⟧)%stn → R), Σ f = op1 (Σ (f ∘ stn_left m n)) (Σ (f ∘ stn_right m n)).
proof: Proof. intros. induction n as [| n IHn]. { change (Σ _) with (@rigunel1 R) at 3. set (a := m + 0). assert (a = m). { apply natplusr0. } assert (e := ! natplusr0 m). rewrite (transport_vecsum e). unfold funcomp. rewrite rigrunax1. apply maponpaths. apply pathsinv0. apply funextfun. intros i. now rewrite <- stn_left_0. } rewrite vecsum_step. assert (e : S (m + n) = m + S n). { apply pathsinv0. apply natplusnsm. } rewrite (transport_vecsum e). rewrite vecsum_step. rewrite <- rigassoc1. apply map_on_two_paths. { rewrite IHn; clear IHn. apply map_on_two_paths. { apply vecsum_eq; intro i. unfold funcomp. apply maponpaths. apply subtypePath_prop. rewrite stn_left_compute. induction e. rewrite idpath_transportf. rewrite dni_last. apply idpath. } { apply vecsum_eq; intro i. unfold funcomp. apply maponpaths. apply subtypePath_prop. rewrite stn_right_compute. unfold stntonat. induction e. rewrite idpath_transportf. rewrite 2? dni_last. apply idpath. } } unfold funcomp. apply maponpaths. apply subtypePath_prop. now induction e. Defined.
imports: UniMath.Foundations.PartA UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Nat UniMath.MoreFoundations.Tactics UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors UniMath.Algebra.RigsAndRings UniMath.Algebra.IteratedBinaryOperations UniMath.Algebra.Matrix UniMath.Algebra.GaussianElimination.Auxiliary