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