proposition: Theorem pluspf_inv2 : forall a b p q, ltT ltM a b -> eqP A eqA n (pX b (pluspf (pX a p) q)) (pluspf (pX a p) (pX b q)).
proof: Proof. Proof using os multA minusA invA divA cs A1. intros a b p q H'; try assumption. rewrite (plusP_inv2 a b p q (pluspf (pX a p) (pX b q))); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)