proposition: Theorem cb_Red_cb2 : 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 (Red L) -> Cb A A0 eqA plusA multA eqA_dec n ltM ltM_dec p L.
proof: Proof. intros p L H'. apply Cb_compo with (L1 := Red L); auto. intros q H'0. apply Red_cb; auto. Qed.
imports: Buchberger(Buch)