proposition: Lemma pi_red_ord : reduction_ordering succ.
proof: Proof. unfold succ. apply IR_reduction_ordering. apply pi_monotone. apply WF_Dgt. Qed.
imports: CoLoR(ATerm ABterm ListUtil VecUtil PositivePolynom AInterpretation ZUtil NaryFunction ARelation RelUtil LogicUtil SN Polynom MonotonePolynom NatUtil ATrs BoundNat AWFMInterpretation ZUtil ACompat AMannaNess)