proposition: Lemma mint_eval_mon_succeq (val : valuation I) k (mi mi' : mint k) : mint_ge mi mi' -> mint_eval val mi >=v mint_eval val mi'.
proof: Proof. intros. unfold mint_eval, add_vectors. simpl. apply (@vec_plus_ge_compat dim). exact (mint_eval_mon_succeq_args _ H). destruct H. hyp. Qed.
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)