proposition: Lemma mat_mult_assoc : forall m n p l (M : matrix m n) (N : matrix n p) (P : matrix p l), M <*> (N <*> P) =m M <*> N <*> P.
proof: Proof. unfold mat_eqA. intros. mat_get_simpl. rewrite !mat_mult_elem, mat_mult_row, mat_mult_col. apply dot_product_assoc. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)