Lemma pulse_prod_is_pulse {n : nat} (f g : stn n -> R) {i : stn n} (H : is_pulse_function i f) : is_pulse_function i (f *pw g). Proof. unfold is_pulse_function in * |- ; intros j. intros neq; unfold pointwise. etrans. { apply maponpaths_2. apply(H j neq). } apply rigmult0x. 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.