proposition: Theorem Cb_stable : forall (a : poly A0 eqA ltM) (Q : list (poly A0 eqA ltM)), Cb A A0 eqA plusA multA eqA_dec n ltM ltM_dec a Q -> stable Q (addEnd A A0 eqA n ltM a Q).
proof: Proof. Proof using os minusA invA divA cs A1. intros a Q H'0; apply stable0; auto. intros a0 H'1. apply Cb_trans with (b := a) (1 := cs); auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)