proposition: Theorem minuspf_eq_inv2 : 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 (invTerm (A:=A) invA (n:=n) a) (minuspf p q)) (minuspf p (pX a q)).
proof: Proof. Proof using plusA os divA cs. intros a p; elim p; auto. intros q H' H'0; rewrite minuspf_pOmults_eq. rewrite minuspf_pOmults_eq; simpl in |- *. apply eqpP1; auto. change (eqTerm (A:=A) eqA (n:=n) (invTerm (A:=A) invA (n:=n) a) (multTerm (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) a)) in |- *. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := invTerm (A:=A) invA (n:=n) (multTerm (A:=A) multA (n:=n) (T1 A1 n) a)); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); auto. intros a0 l H' q H'0 H'1. change (eqP A eqA n (pX (invTerm (A:=A) invA (n:=n) a) (minuspf (pX a0 l) q)) (minuspf (pX a0 l) (pX a q))) in |- *. rewrite <- (minuspf_inv2_eq a0 a l q); auto. apply (canonical_pX_order A A0 eqA) with (l := l); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)