proposition: Theorem Cb_id : forall (a : poly A0 eqA ltM) (Q : list (poly A0 eqA ltM)), In a Q -> Cb a Q.
proof: Proof. Proof using os minusA invA divA cs A1. intros a; case a; simpl in |- *. intros x; case x; auto. intros c Q H'. replace (nil (A:=Term A n)) with (pO A n); auto; apply CombLinear_0; auto. intros a0 l c Q H'. apply CombLinear_id with (1 := cs); auto. change (inPolySet A A0 eqA n ltM (s2p A A0 eqA n ltM (mks A A0 eqA n ltM (pX a0 l) c)) Q) in |- *; apply in_inPolySet; auto. red in |- *; intros H'4; inversion H'4. Qed.
imports: Buchberger(moreCoefStructure)