proposition: Lemma mint_eval_mon_succeq_args : forall k (val : vector vec k) (mi mi' : mint k), mint_ge mi mi' -> add_vectors (Vmap2 mat_vec_prod (args mi) val) >=v add_vectors (Vmap2 mat_vec_prod (args mi') val).
proof: Proof. destruct mi. gen val. clear val. induction args0. intros. destruct mi'. VOtac. unfold mint_eval, add_vectors. simpl. refl. intros. destruct mi' as [const1 args1]. VSntac args1. unfold mint_eval, add_vectors. simpl. destruct H. apply (@vec_plus_ge_compat dim). apply (IHargs0 (Vtail val) (mkMatrixInt const1 (Vtail (args1)))). split. simpl. change args0 with (Vtail (Vcons h args0)). apply Vforall2_tail. hyp. hyp. apply mat_vec_prod_ge_compat. change h with (Vhead (Vcons h args0)). rewrite !Vhead_nth. apply Vforall2_elim_nth. hyp. refl. Qed.
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)