proposition: 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: Proof. rewrite vecsum_left_right, rigcomm1, vecsum_eq_zero. - now rewrite riglunax1. - now rewrite right_part_is_zero. 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