proposition: Lemma vecsum_zero {n} : Σ (@const_vec R n 0%rig) = 0%rig.
proof: Proof. induction n as [ | n IH]. { reflexivity. } rewrite vecsum_step. rewrite rigrunax1. apply IH. 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