Lemma left_inv_matrix_prod_is_left_inv {m n : nat} (A : Matrix R m n) (A' : Matrix R n n) (pa : matrix_left_inverse A) (pb : matrix_left_inverse A') : (matrix_left_inverse (A ** A')). Proof. intros. exists ((pr1 pb) ** (pr1 pa)); simpl. rewrite matrix_mult_assoc, <- (matrix_mult_assoc _ A _). now rewrite (pr2 pa), matlunax2, (pr2 pb). 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.