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