proposition: Theorem pluspf_inv2_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 p (pX a q).
proof: Proof. Proof using os. intros a p; case p; auto. intros q H'0 H'1. rewrite <- pO_pluspf_inv1; auto. rewrite <- pO_pluspf_inv1; auto. intros a0 l q H'0 H'1. change (pX a (pluspf (pX a0 l) q) = pluspf (pX a0 l) (pX a q)) in |- *. apply pluspf_inv2_eq; auto. apply (canonical_pX_order A A0 eqA) with (l := l); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)