proposition: Lemma mat_vec_prod_distr_mat : forall m n (Ml Mr : matrix m n) v, mat_vec_prod (Ml <+> Mr) v =v mat_vec_prod Ml v [+] mat_vec_prod Mr v.
proof: Proof. intros. unfold mat_vec_prod. apply Vforall2_intro_nth. intros. rewrite vector_plus_nth. mat_get_simpl. rewrite !mat_mult_elem. set (a := get_col (Vmap (fun i0 : A => Vcons i0 Vnil) v) access_0). rewrite (dot_product_comm (get_row Ml ip)), (dot_product_comm (get_row Mr ip)), <- dot_product_distr_r, (dot_product_comm a). apply dot_product_mor. 2: refl. clear a. unfold get_row, mat_plus. rewrite Vnth_map2. refl. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)