proposition: Lemma mint_eval_mon_succ : forall (val : valuation I) k (mi mi' : mint k), mint_gt mi mi' -> succ_vec (mint_eval val mi) (mint_eval val mi').
proof: Proof. intros. unfold succ_vec. apply Vforall2_intro_nth. intros. destruct H. eapply gtx_mor. eapply Vforall2_elim_nth; rewrite mint_eval_split; refl. eapply Vforall2_elim_nth. rewrite mint_eval_split. refl. rewrite !vector_plus_nth. apply gtx_plus_compat. apply Vforall2_elim_nth. hyp. rewrite !add_vectors_nth. apply Vfold_left_rev_gtx_compat. intros. rewrite !Vnth_map, !Vnth_map2. set (eval := Vnth (Vbuild (fun i (_ : i < k) => val i)) ip0). apply Vforall2_elim_nth. apply mat_vec_prod_gt_compat. apply Vforall2_elim_nth. hyp. refl. Qed.
imports: CoLoR(AMonAlg Matrix OrdSemiRing VecUtil SN RelUtil LogicUtil AMatrixBasedInt) Coq(Setoid Morphisms)