Lemma pulse_function_sums_to_point { n : nat } (f : ⟦ n ⟧%stn -> R) (i : ⟦ n ⟧%stn) (f_pulse_function : is_pulse_function i f) : Σ f = f i. Proof. destruct (stn_inhabited_implies_succ i) as [n' e_n_Sn']. destruct (!e_n_Sn'). rewrite (vecsum_dni f i). rewrite vecsum_eq_zero. { rewrite riglunax1. apply idpath. } intros k. unfold funcomp. unfold const_vec. assert (i_neq_dni : i ≠ dni i k). {exact (dni_neq_i i k). } intros; destruct (stn_eq_or_neq i (dni i k) ) as [eq | neq]. - apply (stnneq_iff_nopath i (dni i k)) in eq. apply weqtoempty. intros. apply eq. assumption. exact (dni_neq_i i k). - apply f_pulse_function; exact neq. 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.