Lemma matlunax2 : ∏ (m n: nat) (mat : Matrix R n m), (identity_matrix ** mat) = mat. Proof. intros. apply funextfun. intros i. apply funextfun. intros j. unfold matrix_mult, row. use sum_id_pointwise_prod. 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.