proposition: Theorem pO_minusP_inv1 : forall p q : list (Term A n), minusP (pO A n) p q -> q = mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) p.
proof: Proof. intros p; elim p. intros q H'; inversion H'; auto. intros a l H' q H'0; inversion H'0; auto. Qed.
imports: Coq(Arith) Buchberger(LetP)