proposition: Theorem pluspf_inv1_eq : forall a b p q, ltT ltM b a -> pX a (pluspf p (pX b q)) = pluspf (pX a p) (pX b q).
proof: Proof. Proof using os. intros a b p q H'; rewrite (plusP_inv1 a b p q (pluspf (pX a p) (pX b q))); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)