proposition: Theorem plusTerm_is_pX : forall (a : Term A n) (p : list (Term A n)), canonical A0 eqA ltM (pX a p) -> eqP A eqA n (pluspf (pX a (pO A n)) p) (pX a p).
proof: Proof. Proof using os multA minusA invA divA cs A1. intros a p; case p; auto. intros a0 l H'. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pX a (pluspf (pO A n) (a0 :: l))); auto. change (eqP A eqA n (pluspf (pX a (pO A n)) (pX a0 l)) (pX a (pluspf (pO A n) (pX a0 l)))) in |- *. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); apply pluspf_inv1; auto. apply (canonical_pX_order A A0 eqA) with (l := l); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)