proposition: Lemma matrix_inverse_unique {n : nat} (A : Matrix R n n) (B C : matrix_inverse A) : pr1 B = pr1 C.
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors UniMath.Algebra.RigsAndRings UniMath.Algebra.IteratedBinaryOperations UniMath.Algebra.Matrix UniMath.Algebra.Domains_and_Fields UniMath.Algebra.GaussianElimination.Auxiliary UniMath.Algebra.GaussianElimination.Vectors