proposition: Theorem plusP_decomp : forall a p, canonical A0 eqA ltM (pX a p) -> plusP (pX a (pO A n)) p (pX a p).
proof: Proof. intros a p; case p; auto. intros m l H'; try assumption. change (plusP (pX a (pO A n)) (pX m l) (pX a (pX m l))) in |- *. apply mainu1; auto. apply (canonical_pX_order _ A0 eqA) with (l := l); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)