proposition: Lemma monotone_succ : monotone I succ.
proof: Proof. intros f i j i_j vi vj a b ab. split. apply monotone_succeq. destruct ab. hyp. simpl. unfold mi_eval_aux. apply vec_plus_gt_compat_r. rewrite !Vmap_cast, !Vmap_app. simpl. apply vec_add_monotone_map2; try solve [destruct ab; hyp]. intros. unfold MBI.vec_at0. unfold mat_vec_prod. rewrite !Vnth_col_mat, !mat_mult_spec. apply dot_product_mon_r with 0%nat dim_pos. unfold ge. apply Vforall2_intro_nth. intros. apply BigN.le_refl. unfold ge. apply Vforall2_intro_nth. intros. rewrite !get_col_col_mat. destruct ab. apply (Vforall2_elim_nth (R:=ge)). hyp. hyp. rewrite !get_col_col_mat. hyp. apply matrixInt_monotone. apply BigN.le_refl. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil Matrix OrdSemiRing VecUtil AMonAlg SN RelUtil AWFMInterpretation NatUtil BigNUtil AMatrixBasedInt)