proposition: Lemma matrix_right_left_inverse_to_inverse {n : nat} (A : Matrix R n n) : matrix_left_inverse A -> matrix_right_inverse A -> (matrix_inverse A).
proof: Proof. intros lft rght. use tpair; simpl. { apply lft. } split. 2: { apply lft. } rewrite (@matrix_left_inverse_equals_right_inverse n _ n _ lft rght). apply rght. 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