proposition: Theorem plusP_inv2 : forall a b p q s, plusP (pX a p) (pX b q) s -> ltT ltM a b -> s = pX b (pluspf (pX a p) q).
proof: Proof. Proof using os. intros a b p q s H'; inversion_clear H'; intros. absurd (ltT ltM a b); auto. absurd (ltT ltM a b); auto. absurd (ltT ltM a b); auto. apply pX_inj; auto. apply uniq_plusp with (l := (pX a p, q)); simpl in |- *; auto. Qed.
imports: Coq(Arith) Buchberger(LetP)