proposition: Lemma mat_vec_prod_distr_add_vectors : forall m n (M : matrix m n) k v1 v2, (forall i (ip : i < k), mat_vec_prod M (Vnth v1 ip) =v Vnth v2 ip) -> mat_vec_prod M (add_vectors v1) =v add_vectors v2.
proof: Proof. induction k; intros. VOtac. unfold add_vectors. simpl. apply Vforall2_intro_nth. intros. unfold mat_vec_prod. rewrite Vnth_col_mat. unfold zero_vec. rewrite Vnth_const, mat_mult_spec, dot_product_comm, dot_product_zero. refl. apply Vforall_nth_intro. intros. rewrite get_col_col_mat, Vnth_const. refl. VSntac v1. VSntac v2. rewrite !add_vectors_cons, mat_vec_prod_distr_vec, !Vhead_nth. apply vector_plus_mor. rewrite H. refl. rewrite (IHk (Vtail v1) (Vtail v2)). refl. intros. rewrite Vnth_tail, H, Vnth_tail. refl. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)