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