proposition: Theorem divTerm_ppcl : forall (a b : Term A n) (nZa : ~ zeroP (A:=A) A0 eqA (n:=n) a), ~ zeroP (A:=A) A0 eqA (n:=n) b -> eqTerm (A:=A) eqA (n:=n) (ppc a b) (multTerm (A:=A) multA (n:=n) (divTerm (ppc a b) nZa) a).
proof: Proof. Proof using plusA minusA invA cs. intros a b; case a; case b; simpl in |- *; auto. intros a0 m a1 m0 nZa H; split; auto. apply divA_is_multA with (1 := cs); auto. apply ppcm_prop_l. Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)