proposition: Theorem Cb_cons : forall (p : poly A0 eqA ltM) (L : list (poly A0 eqA ltM)), Cb A A0 eqA plusA multA eqA_dec n ltM ltM_dec (nf A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os p L) (p :: L).
proof: Proof. intros p L; unfold nf, LetP in |- *; auto. case (Reducef A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os L p); simpl in |- *; auto. intros x0; case x0; simpl in |- *. intros x c H'. change (CombLinear A A0 eqA plusA multA eqA_dec n ltM ltM_dec (p :: L) (mults (A:=A) multA (n:=n) (unit A A0 A1 eqA divA n ltM (mks A A0 eqA n ltM x c)) x)) in |- *. apply CombLinear_mults1 with (1 := cs); auto. apply unit_nZ with (1 := cs); auto. apply reducestar_cb1 with (1 := cs); auto. Qed.
imports: Buchberger(Buch)