Definition matrix_mult_assoc_statement : UU := ∏ (m n : nat) (mat1 : Matrix R m n) (p : nat) (mat2 : Matrix R n p) (q : nat) (mat3 : Matrix R p q), ((mat1 ** mat2) ** mat3) = (mat1 ** (mat2 ** mat3)).
Require Import UniMath.Foundations.PartA. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Combinatorics.FiniteSequences. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.IteratedBinaryOperations. Require Import UniMath.Algebra.RigsAndRings.