fact: 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)).
imports: UniMath.Foundations.PartA UniMath.MoreFoundations.PartA UniMath.Combinatorics.FiniteSequences UniMath.Algebra.BinaryOperations UniMath.Algebra.IteratedBinaryOperations UniMath.Algebra.RigsAndRings