proposition: Theorem Cb_genPcPf : forall (b : poly A0 eqA ltM) (P Q R : list (poly A0 eqA ltM)), Cb A A0 eqA plusA multA eqA_dec n ltM ltM_dec b R -> (forall a : poly A0 eqA ltM, In a P -> Cb A A0 eqA plusA multA eqA_dec n ltM ltM_dec a R) -> (forall a : poly A0 eqA ltM, In a Q -> Cb A A0 eqA plusA multA eqA_dec n ltM ltM_dec a R) -> forall a : poly A0 eqA ltM, In a (genPcPf b P Q) -> Cb A A0 eqA plusA multA eqA_dec n ltM ltM_dec a R.
proof: Proof. intros b P Q R; unfold genPcPf in |- *; case (genPcPf0 b P Q). intros x H' H'0 H'1 H'2 a H'3. apply Cb_genPcP with (i := b) (P := P) (Q := x) (R := Q); auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)