proposition: Theorem plusP_inv3a : forall a b p q s, eqT a b -> zeroP (A:=A) A0 eqA (n:=n) (plusTerm (A:=A) plusA (n:=n) a b) -> plusP (pX a p) (pX b q) s -> s = pluspf p q.
proof: Proof. Proof using os. intros a b p q s Eqd Z0 H'; inversion_clear H'; intros. absurd (eqT b a); auto. apply eqT_sym; auto. apply uniq_plusp with (l := (p, q)); auto. elim H1; auto. absurd (eqT a b); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)