(R : Ring) (m n p q : nat) : HeteroAssociative (@matrix_mult R m n q) (@matrix_mult R n p q) (@matrix_mult R m p q) (@matrix_mult R m n p). Proof. intros M N P; nrapply path_matrix; intros i j Hi Hj. rewrite 2 entry_Build_Matrix. lhs nrapply path_ab_sum. { intros k Hk. rewrite entry_Build_Matrix. apply rng_sum_dist_l. } lhs nrapply ab_sum_sum. rhs nrapply path_ab_sum. 2: intros k Hk; by rewrite entry_Build_Matrix. nrapply path_ab_sum. intros k Hk. rhs nrapply rng_sum_dist_r. nrapply path_ab_sum. intros l Hl. apply associativity. Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Basics.Decidable. Require Import Types.Sigma. Require Import Spaces.List.Core Spaces.List.Theory Spaces.List.Paths. Require Import Algebra.Rings.Ring Algebra.Rings.Module Algebra.Rings.CRing Require Import abstract_algebra. Require Import WildCat.Core WildCat.Paths. Require Import Modalities.ReflectiveSubuniverse.