proposition: Theorem minuspf_is_pluspf_mults : forall p q : list (Term A n), eqP A eqA n (minuspf p q) (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec p (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) q)).
proof: Proof. Proof using os divA cs. intros p q; try assumption. apply minusP_is_plusP_mults with (p := p) (q := q); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)