proposition: 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: Proof. unfold is_pulse_function in * |- ; intros j. intros neq; unfold pointwise. etrans. { apply maponpaths_2. apply(H j neq). } apply rigmult0x. 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