proposition: Lemma bsucceq'_ok : forall l r, bsucceq' l r = true <-> succeq' l r.
proof: Proof. intros l r. unfold bsucceq', succeq'. apply bcoef_pos_ok. Qed.
imports: CoLoR(APolyInt AMonAlg ZUtil RelUtil PositivePolynom ATrs MonotonePolynom LogicUtil BoolUtil)