proposition: Theorem minuspf_refl : forall p : list (Term A n), eqP A eqA n (minuspf p p) (pO A n).
proof: Proof. Proof using plusA os divA cs. intros p. rewrite (minusP_refl p p (minuspf p p)); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)