proposition: Theorem pluspf_inv3a : forall a b p q, eqT a b -> zeroP (A:=A) A0 eqA (n:=n) (plusTerm (A:=A) plusA (n:=n) a b) -> eqP A eqA n (pluspf 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' Z; try assumption. rewrite (plusP_inv3a a b p q (pluspf (pX a p) (pX b q))); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)