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. 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.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Nat. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.IteratedBinaryOperations. Require Import UniMath.Algebra.Matrix. Require Import UniMath.Algebra.GaussianElimination.Auxiliary.