proposition: Theorem zerop_nf_cb : forall (L : list poly) (p : poly), zerop (nf L p) -> cb L p.
proof: Proof. intros L p H'. apply zerop_elim_cb with (p := nf L p); auto. Qed.
imports: Coq(List Relation_Definitions) Buchberger(LetP)