proposition: Theorem minuspf_zero : forall (a : Term A n) (p q : list (Term A n)), eqP A eqA n (minuspf (pX a p) (pX a q)) (minuspf p q).
proof: Proof. Proof using plusA os divA cs. intros a p q; try assumption. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := minuspf p q); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n). apply minuspf_inv3a; auto. Qed.
imports: Coq(Arith) Buchberger(LetP)