proposition: Theorem genOCPf_stable : forall (a : poly A0 eqA ltM) (P : list (poly A0 eqA ltM)), In a (genOCPf P) -> Cb A A0 eqA plusA multA eqA_dec n ltM ltM_dec a P.
proof: Proof. intros a P; generalize a; elim P; clear a P; simpl in |- *; auto. intros a H; elim H. intros a l H' a0 H'0. apply Cb_genPcPf with (b := a) (P := l) (Q := genOCPf l); auto with datatypes. apply Cb_id with (1 := cs); auto with datatypes. intros; apply Cb_in1 with (1 := cs); auto. apply Cb_id with (1 := cs); auto with datatypes. intros; apply Cb_in1 with (1 := cs); auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)