proposition: Theorem Cb_comp : forall L1 L2 : list (poly A0 eqA ltM), (forall p : poly A0 eqA ltM, In p L1 -> Cb A A0 eqA plusA multA eqA_dec n ltM ltM_dec p L2) -> forall q : poly A0 eqA ltM, Cb A A0 eqA plusA multA eqA_dec n ltM ltM_dec q L1 -> Cb A A0 eqA plusA multA eqA_dec n ltM ltM_dec q L2.
proof: Proof. Proof using os minusA invA divA cs A1. intros L1 L2 H' q; case q; simpl in |- *. intros x H'0 H'1. apply CombLinear_compo with (1 := cs) (L1 := L1); auto. intros q0 H'2. case inPolySet_inv1 with (1 := H'2); auto. intros q1 H; elim H; intros H0 H1; clear H. lapply (H' q1); [ intros H'6 | idtac ]; auto. generalize H'6 H1; case q1; simpl in |- *; auto. intros x0 H'5 H'7 H'8; rewrite H'8; auto. Qed.
imports: Buchberger(Buch)