proposition: Theorem minuspf_pOmults_eq : forall p : list (Term A n), minuspf (pO A n) p = mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) p.
proof: Proof. Proof using os. intros p; apply uniq_minusp with (l := (pO A n, p)); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)