proposition: Theorem pluspf_assoc : forall p q r, canonical A0 eqA ltM p -> canonical A0 eqA ltM q -> canonical A0 eqA ltM r -> eqP A eqA n (pluspf (pluspf p q) r) (pluspf p (pluspf q r)).
proof: Proof. Proof using os multA minusA invA divA cs A1. intros p q r H' H'0 H'1. apply pluspf3_assoc with (l := (p, (q, r))); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)