proposition: Lemma mint_eval_mult_factor : forall k val M (mi : mint k), mint_eval val (mat_matrixInt_prod M mi) =v mat_vec_prod M (mint_eval val mi).
proof: Proof. unfold mint_eval. intros. simpl. autorewrite with arith. rewrite mat_vec_prod_distr_vec. apply vector_plus_mor. refl. set (gen := Vbuild (A:=vec) (fun i (_ : i < k) => dom2vec (val i))). rewrite (mat_vec_prod_distr_add_vectors M (Vmap2 mat_vec_prod (args mi) gen) (Vmap2 mat_vec_prod (Vmap (mat_mult M) (args mi)) gen)). refl. intros. rewrite !Vnth_map2, Vnth_map. unfold M.mat_vec_prod. rewrite vec_to_col_mat_idem. apply get_col_mor. rewrite mat_mult_assoc. refl. Qed.
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)