proposition: Theorem order_pluspf : forall (l1 l2 : list (Term A n)) (a : Term A n), canonical A0 eqA ltM (pX a l1) -> canonical A0 eqA ltM (pX a l2) -> canonical A0 eqA ltM (pX a (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec l1 l2)).
proof: Proof. Proof using os. intros l1 l2 a H' H'0. apply order_plusP with (1 := os) (plusA := plusA) (l1 := l1) (l2 := l2); auto. apply pluspf_is_plusP; auto. apply canonical_pluspf; auto. apply canonical_imp_canonical with (a := a); auto. apply canonical_imp_canonical with (a := a); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)