proposition: Theorem ppc_com : forall a b : Term A n, eqTerm (A:=A) eqA (n:=n) (ppc a b) (ppc b a).
proof: Proof. Proof using plusA multA minusA invA divA cs A0. intros a b; case a; case b; simpl in |- *; auto. intros a0 m a1 m0; split; auto. apply ppcm_com; auto. Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)