proposition: Theorem minusP_refl : forall p q r : list (Term A n), minusP p q r -> p = q -> r = pO A n.
proof: Proof. Proof using plusA os divA cs. intros p q r H'; elim H'; auto. intros l1 H'0; rewrite <- H'0; simpl in |- *; auto. intros a1 a2 l1 l2 l3 H'0 H'1 H'2 H'3; generalize H'0. rewrite (pX_invl A n a1 a2 l1 l2); auto; intros Ord. absurd (ltT ltM a2 a2); auto. intros a1 a2 l1 l2 l3 H'0 H'1 H'2 H'3 H'4. apply H'1; auto. apply pX_invr with (a := a1) (b := a2); auto. intros a1 a2 l1 l2 l3 H'0 H'1 H'2 H'3 H'4; elim H'3; auto. rewrite (pX_invl A n a1 a2 l1 l2); auto. intros a1 a2 l1 l2 l3 H'0 H'1 H'2 H'3; generalize H'0. rewrite (pX_invl A n a1 a2 l1 l2); auto; intros Ord. absurd (ltT ltM a2 a2); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)