proposition: Lemma mint_eval_const : forall val k (c : vec), mint_eval (k:=k) val (mkMatrixInt c (combine_matrices Vnil)) =v c.
proof: Proof. intros. unfold mint_eval. simpl. autorewrite with arith. trans (c [+] @zero_vec dim). apply vector_plus_mor. refl. apply add_vectors_zero. apply Vforall_nth_intro. intros. rewrite Vnth_map2, combine_matrices_nil, Vnth_const. unfold M.mat_vec_prod. apply Vforall2_intro_nth. intros. rewrite Vnth_col_mat. trans (get_elem (zero_matrix dim 1) ip0 access_0). apply get_elem_mor. apply zero_matrix_mult_l. unfold zero_matrix. rewrite mat_build_elem. unfold zero_vec. rewrite Vnth_const. refl. apply vector_plus_zero_r. Qed.
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)