proposition: Lemma monotone_succeq : monotone I succeq.
proof: Proof. intros f i j i_j vi vj a b ab. simpl. unfold mi_eval, mi_eval_aux, succeq. simpl. apply (@vec_plus_ge_compat_r dim). rewrite !Vmap_cast, !Vmap_app. simpl. apply vec_add_weak_monotone_map2; trivial. intros. unfold succeq. apply Vforall2_intro_nth. intros. unfold M.mat_vec_prod. rewrite !Vnth_col_mat. apply mat_mult_mon. apply mat_ge_refl. intros x y xp yp. rewrite !vec_to_col_mat_spec. apply Vforall2_elim_nth. hyp. Qed.
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)