proposition: Lemma pi_compat : forall R, lforall (fun r => coef_pos (rulePoly_gt r)) R -> compat succ R.
proof: Proof. unfold compat. intros. set (rho := mkRule l r). change (succ (lhs rho) (rhs rho)). apply pi_compat_rule. apply (lforall_in H H0). Qed.
imports: CoLoR(ATerm ABterm ListUtil VecUtil PositivePolynom AInterpretation ZUtil NaryFunction ARelation RelUtil LogicUtil SN Polynom MonotonePolynom NatUtil ATrs BoundNat AWFMInterpretation ZUtil ACompat AMannaNess)