proposition: Lemma succ_succeq_compat : absorbs_left succ succeq.
proof: Proof. intros x z xz. destruct xz as [y [xy yz]]. split. apply trans_succeq with y. hyp. destruct yz. hyp. apply ge_gt_compat with (Vnth (dom2vec y) dim_pos). unfold MBI.vec_at0. apply Vforall2_elim_nth. hyp. destruct yz. hyp. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil Matrix OrdSemiRing VecUtil AMonAlg SN RelUtil AWFMInterpretation NatUtil AMatrixBasedInt)