proposition: Lemma pi_absorb : absorbs_left succ succ_eq.
proof: Proof. unfold absorbs_left, inclusion. intros. do 2 destruct H. unfold succ_eq, succ, IR, Dge, Dgt, transp, Dle, Dlt in *. intro. eapply Z.lt_le_trans. apply H0. apply H. Qed.
imports: CoLoR(ATerm ABterm ListUtil VecUtil PositivePolynom AInterpretation ZUtil NaryFunction ARelation RelUtil LogicUtil SN Polynom MonotonePolynom NatUtil ATrs BoundNat AWFMInterpretation ZUtil ACompat AMannaNess)