proposition: Lemma matrix_add_assoc {m n : nat} (mat1 : Matrix R m n) (mat2 : Matrix R m n) (mat3 : Matrix R m n) : matrix_add (matrix_add mat1 mat2) mat3 = matrix_add mat1 (matrix_add mat2 mat3).
proof: Proof. apply entrywise_assoc, rigassoc1. 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