proposition: Theorem minuspf_inv1 : forall (a b : Term A n) (p q : list (Term A n)), ltT ltM b a -> eqP A eqA n (pX a (minuspf p (pX b q))) (minuspf (pX a p) (pX b q)).
proof: Proof. Proof using plusA os divA cs. intros a b p q H'; try assumption. rewrite (minusP_inv1 a b p q (minuspf (pX a p) (pX b q))); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)