proposition: Lemma mi_eval_cons : forall n (mi : mint (S n)) v vs, mi_eval_aux mi (Vcons v vs) =v mat_vec_prod (Vhead (args mi)) v [+] mi_eval_aux (mkMatrixInt (const mi) (Vtail (args mi))) vs.
proof: Proof. intros. unfold mi_eval_aux. simpl. rewrite vector_plus_assoc. apply vector_plus_mor. apply vector_plus_comm. refl. Qed.
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)