Lemma vecsum_to_leftsum {n m' n' : nat} (p : m' + n' = n) (f : ⟦ m' + n' ⟧%stn -> R) (right_part_is_zero : (f ∘ stn_right m' n') = const_vec 0%rig): Σ f = Σ (f ∘ stn_left m' n' ). Proof. rewrite vecsum_left_right, rigcomm1, vecsum_eq_zero. - now rewrite riglunax1. - now rewrite right_part_is_zero. 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.