proposition: Theorem minuspf_refl_eq : forall p : list (Term A 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)