proposition: Lemma mat_vec_prod_distr_vec : forall m n (M : matrix m n) v1 v2, mat_vec_prod M (v1 [+] v2) =v mat_vec_prod M v1 [+] mat_vec_prod M v2.
proof: Proof. intros. unfold mat_vec_prod. apply Vforall2_intro_nth. intros. rewrite vector_plus_nth. mat_get_simpl. rewrite !mat_mult_elem, <- dot_product_distr_r. apply dot_product_mor. refl. apply Vforall2_intro_nth. intros. unfold get_col. rewrite !Vnth_map. simpl. rewrite vector_plus_nth. unfold vector_plus. rewrite Vnth_map2, !Vnth_map. refl. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)