proposition: Lemma succeq'_dec : rel_dec succeq'.
proof: Proof. intros l r. unfold succeq'. eapply dec. apply bcoef_pos_ok. Defined.
imports: CoLoR(APolyInt AMonAlg ZUtil RelUtil PositivePolynom ATrs MonotonePolynom LogicUtil BoolUtil)