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