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