proposition: Theorem minuspf_pO_is_eqP : forall p q : list (Term A n), eqP A eqA n (minuspf p q) (pO A n) -> eqP A eqA n p q.
proof: Proof. Proof using plusA divA cs. intros p q H'. apply minusP_pO_is_eqP with (r := minuspf p q); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)