proposition: Lemma RO_lem : forall (a : poly A0 eqA ltM) (P : list (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 a P) -> RO (addEnd A A0 eqA n ltM (nf A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os a P) P) P.
proof: Proof. intros a P H'; rewrite addEnd_app. apply RO0; auto. Qed.
imports: Coq(List) Buchberger(ListProps Bar Dickson Monomials)