proposition: Lemma mint_eval_split : forall val k (mi : mint k), let coefs := Vbuild (fun i (ip : i < k) => dom2vec (val i)) in mint_eval val mi =v AMatrixBasedInt.const mi [+] add_vectors (Vmap2 mat_vec_prod (args mi) coefs).
proof: Proof. intros. unfold mint_eval, add_vectors. simpl. rewrite vector_plus_comm. refl. Qed.
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)