Lemma is_pulse_function_stdb_vector { n : nat } (i : ⟦ n ⟧%stn) : is_pulse_function i (stdb_vector i). Proof. intros j i_neq_j. unfold stdb_vector, pointwise. now rewrite (stn_eq_or_neq_right i_neq_j). 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.