proposition: Lemma vecsum_add {n} (v1 v2 : (⟦ n ⟧)%stn -> R) : Σ (v1 +pw v2) = (Σ v1 + Σ v2)%rig.
proof: 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.
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