proposition: 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: 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.
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