Lemma col_inj {X : UU} (m n : nat) (mat1 mat2 : Matrix X m n) : (∏ i : (stn n), col mat1 i = col mat2 i) -> mat1 = mat2. Proof. intro H. apply funextfun; intro i; apply funextfun; intro j. specialize (H j). apply toforallpaths in H. apply H. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. 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.Domains_and_Fields. Require Import UniMath.Algebra.GaussianElimination.Auxiliary. Require Import UniMath.Algebra.GaussianElimination.Vectors.