proposition: Theorem Cb_cons_addEnd : forall (L : list (poly A0 eqA ltM)) (p q : poly A0 eqA ltM), Cb A A0 eqA plusA multA eqA_dec n ltM ltM_dec q (p :: L) -> Cb A A0 eqA plusA multA eqA_dec n ltM ltM_dec q (addEnd A A0 eqA n ltM p L).
proof: Proof. Proof using os minusA invA divA cs A1. intros L p q H; apply Cb_incl with (1 := cs) (P := p :: L); auto. elim L; simpl in |- *; auto. intros a l H0 a0 H1; elim H1; clear H1; intros H1; auto. case H1; auto. Qed.
imports: Buchberger(Buch)