proposition: Lemma vecsum_eq {n : nat} (f g : ⟦ n ⟧%stn -> R) : f ~ g -> Σ f = Σ g.
proof: 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.
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