Lemma sum_stdb_vector_pointwise_prod { n : nat } (v : Vector R n) (i : ⟦ n ⟧%stn) : Σ (stdb_vector i *pw v) = (v i). Proof. etrans. { apply (pulse_function_sums_to_point _ i) , (pulse_prod_is_pulse _ _ ) , is_pulse_function_stdb_vector. } unfold pointwise, stdb_vector. rewrite stn_eq_or_neq_refl. apply riglunax2. 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.