fact: Definition mat_mult m n p (L : matrix m n) (R : matrix n p) := mat_build (fun i j ip jp => dot_product (get_row L ip) (get_col R jp)).
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)