proposition: Lemma matrunax2 : ∏ (m n : nat) (mat : Matrix R m n), (mat ** identity_matrix) = mat.
proof: 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.
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