proposition: Theorem ppc_multTerm_divP : forall a b : Term A n, ~ zeroP (A:=A) A0 eqA (n:=n) a -> ~ zeroP (A:=A) A0 eqA (n:=n) b -> divP (multTerm (A:=A) multA (n:=n) a b) (ppc a b).
proof: Proof. Proof using plusA minusA invA eqA_dec cs. intros a b H' H'0. elim ppc_is_ppcm; auto. Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)