proposition: Theorem pluspf_is_plusP : forall l1 l2, plusP l1 l2 (pluspf l1 l2).
proof: Proof. intros l1 l2; try assumption. unfold pluspf in |- *; case (plusp (l1, l2)); simpl in |- *; auto. Qed.
imports: Coq(Arith) Buchberger(LetP)