Lemma vecsum_eq {n : nat} (f g : ⟦ n ⟧%stn -> R) : f ~ g -> Σ f = Σ g. Proof. intros H. induction n as [|n IH]; try apply idpath. rewrite 2 vecsum_step. induction (H lastelement). apply (maponpaths (λ i, op1 i (f lastelement))). apply IH; intro x; apply H. 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.