Lemma matrunax2 : ∏ (m n : nat) (mat : Matrix R m n), (mat ** identity_matrix) = mat. Proof. intros m n mat. apply funextfun. intros i. apply funextfun. intros j. unfold matrix_mult. rewrite (pulse_function_sums_to_point _ j); rewrite <- (symmetric_mat_row_eq_col _ _ identity_matrix_symmetric); unfold pointwise, row. - now rewrite id_mat_ii, rigrunax2. - intros k j_neq_k; now rewrite (id_mat_ij _ _ j_neq_k), rigmultx0. 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.