proposition: Theorem minuspf_pO_refl : forall p : list (Term A n), eqP A eqA n (minuspf p (pO A n)) p.
proof: Proof. Proof using plusA os divA cs. intros p; apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := 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)) (pO A n))); auto; simpl in |- *; auto. Qed.
imports: Coq(Arith) Buchberger(LetP)