proposition: 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: Proof. intro H. apply funextfun; intro i; apply funextfun; intro j. specialize (H j). apply toforallpaths in H. apply H. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors UniMath.Algebra.RigsAndRings UniMath.Algebra.IteratedBinaryOperations UniMath.Algebra.Matrix UniMath.Algebra.Domains_and_Fields UniMath.Algebra.GaussianElimination.Auxiliary UniMath.Algebra.GaussianElimination.Vectors