proposition: Theorem pluspf_inv1_eqa : forall a p q, canonical A0 eqA ltM (pX a p) -> canonical A0 eqA ltM (pX a q) -> pX a (pluspf p q) = pluspf (pX a p) q.
proof: Proof. Proof using os. intros a p q; case q; auto. rewrite <- pO_pluspf_inv2; auto. rewrite <- pO_pluspf_inv2; auto. intros a0 l H'0 H'1. change (pX a (pluspf p (pX a0 l)) = pluspf (pX a p) (pX a0 l)) in |- *. apply pluspf_inv1_eq; auto. apply (canonical_pX_order _ A0 eqA) with (l := l); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)