proposition: Lemma succ_succeq_compat : absorbs_left succ succeq.
proof: Proof. intros x z xz. destruct xz as [y [xy yz] ]. unfold succ, succ_vec. apply Vforall2_intro_nth. intros. apply ge_gtx_compat with (Vnth (dom2vec y) ip). apply Vforall2_elim_nth. hyp. apply Vforall2_elim_nth. hyp. Qed.
imports: CoLoR(AMonAlg Matrix OrdSemiRing VecUtil SN RelUtil LogicUtil AMatrixBasedInt) Coq(Setoid Morphisms)