proposition: Theorem Cb_in : forall (a b : poly A0 eqA ltM) (Q : list (poly A0 eqA ltM)), Cb a Q -> Cb a (addEnd b Q).
proof: Proof. Proof using os minusA invA divA cs A1. intros a b Q H'. apply Cb_incl with (P := Q); simpl in |- *; auto. intros a0 H'0; apply addEnd_id2; auto. Qed.
imports: Buchberger(moreCoefStructure)