proposition: Lemma succ_succeq_compat : absorbs_left Dgt Dge.
proof: Proof. 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: Coq(Program) CoLoR(ListUtil LogicUtil ZUtil VecUtil Problem ATrs SN APolyInt Polynom RelUtil MonotonePolynom PositivePolynom NaryFunction MonAlgChecker IntBasedChecker Proof OptUtil AWFMInterpretation)