proposition: Lemma monotone_succ : PolyStrongMonotone trsInt -> AWFMInterpretation.monotone I succ.
proof: Proof. unfold I. apply pi_monotone. Qed.
imports: CoLoR(APolyInt AMonAlg ZUtil RelUtil PositivePolynom ATrs MonotonePolynom LogicUtil BoolUtil)