proposition: Theorem pluspf_inv3b_eq : forall a b p q, eqT a b -> ~ zeroP (A:=A) A0 eqA (n:=n) (plusTerm (A:=A) plusA (n:=n) a b) -> pX (plusTerm (A:=A) plusA (n:=n) a b) (pluspf p q) = pluspf (pX a p) (pX b q).
proof: Proof. Proof using os. intros a b p q H' H1'; rewrite (plusP_inv3b a b p q (pluspf (pX a p) (pX b q))); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)