proposition: Theorem inv_prop : forall (a : Term A n) (p q : list (Term A n)), canonical A0 eqA ltM (pX a p) -> minuspf p (pX a q) = pX (inv p a) (minuspf p q).
proof: Proof. Proof using os. intros a p q; case p; simpl in |- *; auto. intros H'. change (minuspf (pO A n) (pX a q) = pX (multTerm (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) a) (minuspf (pO A n) q)) in |- *. rewrite (minuspf_pOmults_eq (pX a q)); simpl in |- *; auto. rewrite (minuspf_pOmults_eq q); simpl in |- *; auto. intros a0 l H'. change (minuspf (pX a0 l) (pX a q) = pX (invTerm (A:=A) invA (n:=n) a) (minuspf (pX a0 l) 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)