proposition: Theorem olist_ltT : forall (l : list (Term A n)) (a b : Term A n), olist (l ++ pX a (pX b pO)) -> ltT b a.
proof: Proof. unfold ltT, olist in |- *; simpl in |- *; auto. intros l a b. rewrite (fP_app l (pX a (pX b pO))); simpl in |- *; auto. intros H'. elim (dist_Desc_concat _ ltM (fP l) (consA (T2M a) (consA (T2M b) nilA))); [ intros H'5 H'6; try exact H'6 | idtac ]; auto. simple inversion H'6. discriminate H. discriminate H. elim (app2_inv y x (T2M a) (T2M b) l0); [ intros H'8 H'9 | idtac ]; auto. rewrite H'9; rewrite H'8; auto. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)