{R : Ring} {m n p : nat} : HeteroAssociative (@matrix_lact R m p) (@matrix_mult R m n p) (@matrix_mult R m n p) (@matrix_lact R m n). Proof. intros r M N. snrapply path_matrix. intros i j Hi Hj. rewrite !entry_Build_Matrix, !entry_Build_Vector. lhs nrapply rng_sum_dist_l. snrapply path_ab_sum. intros k Hk; cbn. rewrite !entry_Build_Matrix. snrapply rng_mult_assoc. 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.