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. 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.
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.