proposition: Lemma identity_matrix_unique_left {m : nat} (Z : Matrix R m m) : (∏ n : nat, ∏ A : (Matrix R m n), (Z ** A) = A) -> Z = identity_matrix.
proof: Proof. intros impl. etrans. { apply pathsinv0, matrunax2. } apply impl. 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