proposition: 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: Proof. etrans. 2: { apply pathsinv0, vecsum_ldistr. } apply vecsum_eq. intro i. apply rigassoc2. 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