proposition: Theorem minuspf_is_minusP : forall l1 l2 : list (Term A n), minusP l1 l2 (minuspf l1 l2).
proof: Proof. intros l1 l2; try assumption. unfold minuspf in |- *; case (minuspp (pair l1 l2)); simpl in |- *; auto. Qed.
imports: Coq(Arith) Buchberger(LetP)