proposition: Theorem minuspf_inv2_eq : forall (a b : Term A n) (p q : list (Term A n)), ltT ltM a b -> pX (invTerm (A:=A) invA (n:=n) b) (minuspf (pX a p) q) = minuspf (pX a p) (pX b q).
proof: Proof. Proof using os. intros a b p q H'; try assumption. rewrite (minusP_inv2 a b p q (minuspf (pX a p) (pX b q))); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)