Lemma vecsum_add {n} (v1 v2 : (⟦ n ⟧)%stn -> R) : Σ (v1 +pw v2) = (Σ v1 + Σ v2)%rig. Proof. induction n as [| n IH]. - cbn. apply pathsinv0, riglunax1. - rewrite 3 vecsum_step. etrans. { apply maponpaths_2. apply IH. } refine (rigassoc1 _ _ _ _ @ _ @ !rigassoc1 _ _ _ _). apply maponpaths. refine (!rigassoc1 _ _ _ _ @ _ @ rigassoc1 _ _ _ _). apply maponpaths_2. apply rigcomm1. 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.