proposition: Theorem pluspf_com : forall p q, eqP A eqA n (pluspf p q) (pluspf q p).
proof: Proof. Proof using os multA minusA invA divA cs A1. intros p q; apply (plusP_com p q (pluspf p q) (pluspf q p)); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)