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