proposition: Lemma vecsum_step {n : nat} (f : ⟦ S n ⟧%stn -> R) : Σ f = (Σ (f ∘ (dni lastelement)) + f lastelement)%rig.
proof: Proof. intros; apply iterop_fun_step; apply riglunax1. 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