proposition: Theorem divp_id : forall p : poly A0 eqA ltM, ~ zerop A A0 eqA n ltM p -> divp A A0 eqA multA divA n ltM p p.
proof: Proof. Proof using plusA minusA invA cs A1. intros p; case p; auto. intros x; case x; simpl in |- *; auto. intros a l H' J. cut (~ zeroP (A:=A) A0 eqA (n:=n) a); [ intros Z | idtac ]. apply divTerm_def with (nZb := Z). apply canonical_nzeroP with (p := l) (ltM := ltM); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := multTerm (A:=A) multA (n:=n) (T1 A1 n) a); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply canonical_nzeroP with (p := l) (ltM := ltM); auto. Qed.
imports: Buchberger(Buch)