proposition: Theorem zerop_nf_cb : forall (L : list (poly A0 eqA ltM)) (p : poly A0 eqA ltM), zerop A A0 eqA n ltM (nf A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os p L) -> Cb A A0 eqA plusA multA eqA_dec n ltM ltM_dec p L.
proof: Proof. intros L p H'. apply zerop_elim_cb with (p := nf A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os p L); auto. apply Cb_nf. Qed.
imports: Buchberger(Buch)