proposition: Theorem olist_pX_order : forall l a b, olist (pX a (pX b l)) -> ltT b a.
proof: Proof. intros l a b H'. elim (dist_Desc_concat _ ltM (consA (T2M a) (consA (T2M b) nilA)) (fP l)); [ intros H'5 H'6 | idtac ]; auto. apply olist_ltT with (l := pO); auto. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)