Lemma two_pulse_function_sums_to_points { n : nat } (f : ⟦ n ⟧%stn -> R) (i : ⟦ n ⟧%stn) (j : ⟦ n ⟧%stn) (ne_i_j : i ≠ j) (f_two_pulse : ∏ (k: ⟦ n ⟧%stn), (k ≠ i) -> (k ≠ j) -> (f k = 0%rig)) : (Σ f = f i + f j)%rig. Proof. assert (H : f = (scalar_lmult_vec (f i) (stdb_vector i)) +pw (scalar_lmult_vec (f j) (stdb_vector j))). { apply funextfun. intros k. unfold stdb_vector, scalar_lmult_vec, vector_fmap, pointwise. destruct (stn_eq_or_neq i k) as [i_eq_k | i_neq_k]. - destruct (stn_eq_or_neq j k) as [j_eq_k | j_neq_k]; destruct i_eq_k. + destruct j_eq_k. now apply isirrefl_natneq in ne_i_j. + now rewrite rigmultx0, rigrunax1, rigrunax2. - rewrite rigmultx0, riglunax1. destruct (stn_eq_or_neq j k) as [j_eq_k | j_neq_k]. + now rewrite rigrunax2, j_eq_k. + rewrite rigmultx0; apply f_two_pulse; now apply issymm_natneq. } etrans. { apply maponpaths, H. } etrans. { apply vecsum_add. } apply maponpaths_12; rewrite <- vecsum_ldistr, stdb_vector_sums_to_1; apply rigrunax2. 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.