proposition: Lemma succ_succeq_compat : absorbs_left succ succeq.
proof: Proof. unfold succ, succeq. intros p q pq. destruct pq as [r [pr rq]]. unfold Dgt, Dlt, transp. apply Z.lt_le_trans with (val r); auto. Qed.
imports: CoLoR(APolyInt AMonAlg ZUtil RelUtil PositivePolynom ATrs MonotonePolynom LogicUtil BoolUtil)