proposition: Theorem olistOne : forall a b : Term A n, ltT b a -> olist (pX a (pX b pO)).
proof: Proof. unfold olist, ltT in |- *; simpl in |- *; auto. intros a b H'. generalize (d_conc _ ltM (T2M b) (T2M a) nilA); simpl in |- *; auto. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)