proposition: Theorem divP_ppcr : forall a b : Term A n, ~ zeroP (A:=A) A0 eqA (n:=n) a -> ~ zeroP (A:=A) A0 eqA (n:=n) b -> divP (ppc a b) b.
proof: Proof. Proof using plusA minusA invA cs. intros a b H' H'0; try assumption. lapply (ppc_is_ppcm a b); [ intros H'3; lapply H'3; clear H'3; [ intros H'4 | idtac ] | idtac ]; auto; auto. inversion H'4; auto. Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)