Lemma vecsum_scalar_lmult {m} (s : R) (v w : Vector R m) : Σ (scalar_lmult_vec s v *pw w) = (s * Σ (v *pw w))%rig. Proof. etrans. 2: { apply pathsinv0, vecsum_ldistr. } apply vecsum_eq. intro i. apply rigassoc2. 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.