proposition: Lemma is_pulse_function_stdb_vector { n : nat } (i : ⟦ n ⟧%stn) : is_pulse_function i (stdb_vector i).
proof: Proof. intros j i_neq_j. unfold stdb_vector, pointwise. now rewrite (stn_eq_or_neq_right i_neq_j). Defined.
imports: UniMath.Foundations.PartA UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Nat UniMath.MoreFoundations.Tactics UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors UniMath.Algebra.RigsAndRings UniMath.Algebra.IteratedBinaryOperations UniMath.Algebra.Matrix UniMath.Algebra.GaussianElimination.Auxiliary