proposition: Theorem minuspf_eq_inv1 : forall (a : Term A n) (p q : list (Term A n)), canonical A0 eqA ltM (pX a p) -> canonical A0 eqA ltM (pX a q) -> eqP A eqA n (pX a (minuspf p q)) (minuspf (pX a p) q).
proof: Proof. Proof using plusA os divA cs. intros a p q; case q; simpl in |- *; auto. intros H' H'0; rewrite minuspf_pO_refl_eq; rewrite minuspf_pO_refl_eq; auto. intros a0 l H' H'0. change (eqP A eqA n (pX a (minuspf p (pX a0 l))) (minuspf (pX a p) (pX a0 l))) in |- *; apply minuspf_inv1; auto. apply (canonical_pX_order A A0 eqA) with (l := l); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)