proposition: Lemma matrix_left_inverse_equals_right_inverse {m n k: nat} (A : Matrix R n n) (lft : matrix_left_inverse A) (rght : matrix_right_inverse A) : pr1 lft = pr1 rght.
proof: Proof. destruct lft as [? islft]. destruct rght as [rght isrght]; simpl. pose (H0 := matlunax2 n n rght). now rewrite <- islft, matrix_mult_assoc, isrght, matrunax2 in H0. 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