proposition: Theorem Cb_genPcP : forall (i : poly A0 eqA ltM) (P Q R S : list (poly A0 eqA ltM)), genPcP i P R Q -> Cb A A0 eqA plusA multA eqA_dec n ltM ltM_dec i S -> (forall a : poly A0 eqA ltM, In a P -> Cb A A0 eqA plusA multA eqA_dec n ltM ltM_dec a S) -> (forall a : poly A0 eqA ltM, In a R -> Cb A A0 eqA plusA multA eqA_dec n ltM ltM_dec a S) -> forall a : poly A0 eqA ltM, In a Q -> Cb A A0 eqA plusA multA eqA_dec n ltM ltM_dec a S.
proof: Proof. intros i P Q R S H'; elim H'; simpl in |- *; auto. intros L L1 L2 L3 a i0 H'0 H'1 H'2 H'3 H'4 H'5 a0 H'6. case (addEnd_cons A A0 eqA n ltM) with (1 := H'6); auto; intros H'7. rewrite H'7; auto. apply Cb_sp; auto. apply H'2; auto. intros a1 H'8. apply H'4; auto. right. generalize (slicef_incl i0 a L1); unfold slicef in |- *; rewrite H'0; auto. intros L L1 L2 L3 a i0 H'0 H'1 H'2 H'3 H'4 H'5 a0 H'6; auto. apply H'2; auto. intros a1 H'7. apply H'4; auto. generalize (slicef_incl i0 a L1); unfold slicef in |- *; rewrite H'0; auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)