proposition: Theorem OBuch_Stable : forall P Q R : list (poly A0 eqA ltM), OBuch P Q R -> (forall a : poly A0 eqA ltM, In a Q -> Cb A A0 eqA plusA multA eqA_dec n ltM ltM_dec a P) -> stable P R.
proof: Proof. intros P Q R H'; elim H'; simpl in |- *; auto. intros a aP Q0 R0 H'0 H'1 H'2 H'3. apply stable_trans with (y := addEnd A A0 eqA n ltM (nf A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os a aP) aP); auto. apply stable0; auto. intros a0 H'4. apply Cb_trans with (1 := cs) (b := nf A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os a aP); auto. apply nf_Cb; auto. apply H'1; auto. intros a0 H'4. apply Cb_genPcPf with (b := nf A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os a aP) (P := aP) (Q := Q0); auto. apply Cb_id with (1 := cs); auto. intros; apply Cb_in with (1 := cs); auto. apply Cb_id 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)