proposition: Theorem canonical_pluspf : forall l1 l2, canonical A0 eqA ltM l1 -> canonical A0 eqA ltM l2 -> canonical A0 eqA ltM (pluspf l1 l2).
proof: Proof. Proof using os. intros l1 l2 H' H'0; generalize (pluspf_is_plusP l1 l2); intros u1. apply canonical_plusP with (l1 := l1) (l2 := l2); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)