Lemma stdb_vector_sums_to_1 { n : nat } (i : ⟦ n ⟧%stn) : Σ (@stdb_vector R n i) = 1%rig. Proof. etrans. { apply (pulse_function_sums_to_point _ i), is_pulse_function_stdb_vector. } unfold stdb_vector; now rewrite stn_eq_or_neq_refl. 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.