Lemma vecsum_rdistr: ∏ (n : nat) (vec : Vector R n) (s : R), op2 (Σ vec) s = Σ (scalar_rmult_vec vec s). Proof. intros. induction n as [| n IH]. - apply rigmult0x. - rewrite 2 vecsum_step. rewrite rigrdistr. 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.