Lemma matrix_inverse_unique {n : nat} (A : Matrix R n n) (B C : matrix_inverse A) : pr1 B = pr1 C. Proof. assert (eq : pr1 B = ((pr1 B) ** (A ** (pr1 C)))). { rewrite (pr1 (pr2 C)). now rewrite matrunax2. } rewrite eq, <- matrix_mult_assoc, (pr2 (pr2 B)). now rewrite matlunax2. 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.