proposition: Theorem cb_Red_cb1 : forall (p : poly A0 eqA ltM) (L : list (poly A0 eqA ltM)), Cb A A0 eqA plusA multA eqA_dec n ltM ltM_dec p L -> Cb A A0 eqA plusA multA eqA_dec n ltM ltM_dec p (Red L).
proof: Proof. intros p L H'. apply Cb_compo with (L1 := L); auto. intros q H'0. apply Cb_Red; auto. Qed.
imports: Buchberger(Buch)