proposition: Lemma succ_succeq_compat : absorbs_left succ succeq.
proof: Proof. intros x z xz val. apply succ_succeq_compat. destruct xz as [y [ge_xy gt_yz]]. exists (term_int val y). split; auto. Qed.
imports: CoLoR(ATrs LogicUtil ARelation RelUtil SN ListUtil AMannaNess ACompat BoolUtil BoundNat) CoLoR(AMonAlg)