Lemma vecsum_ldistr : ∏ (n : nat) (vec : Vector R n) (s : R), op2 s (Σ vec) = Σ (scalar_lmult_vec s vec). Proof. intros. induction n as [| n IH]. - simpl. apply rigmultx0. - rewrite 2 vecsum_step. rewrite rigldistr. apply maponpaths_2, IH. 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.