proposition: Lemma mat_mult_spec : forall m n p (M : matrix m n) (N : matrix n p) i (ip : i < m) j (jp : j < p), get_elem (M <*> N) ip jp = dot_product (get_row M ip) (get_col N jp).
proof: Proof. intros. mat_get_simpl. rewrite mat_mult_elem. refl. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)