proposition: Theorem olist_imp_olist : forall l a b, olist (pX a (pX b l)) -> olist (pX a l).
proof: Proof. Proof using os. intros l; case l. intros a b H'. elim (dist_Desc_concat _ ltM (consA (T2M a) nilA) (consA (T2M b) nilA)); [ intros H'5 H'6 | idtac ]; auto. intros b l0 a b0 H'. apply olist_cons; auto. apply ltT_trans with (y := b0). apply olist_pX_order with (l := l0); auto. apply olist_X with (a := a); auto. apply olist_pX_order with (l := b :: l0); auto. apply olist_X with (a := b0); auto. apply olist_X with (a := a); auto. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)