proposition: Theorem minusP_pO_is_eqP : forall p q r : list (Term A n), minusP p q r -> eqP A eqA n r (pO A n) -> eqP A eqA n p q.
proof: Proof. Proof using plusA divA cs. intros p q r H'; elim H'; auto. intros l1; case l1; simpl in |- *; auto. intros t l H; inversion H. intros a1 a2 l1 l2 l3 H H0 H1 H2; inversion H2. intros a1 a2 l1 l2 l3 H H0 H1 H2 H3. apply eqpP1; auto. apply zerop_is_eqTerm; auto. intros a1 a2 l1 l2 l3 H H0 H1 H2 H3; inversion H3. intros a1 a2 l1 l2 l3 H H0 H1 H2; inversion H2. Qed.
imports: Coq(Arith) Buchberger(LetP)