proposition: Lemma fltP : forall p q, ltP p q -> Ltl _ ltM (fP p) (fP q).
proof: Proof. intros p q H'; elim H'; auto. simpl in |- *; intros; apply (Lt_nil (mon n)); auto. simpl in |- *; intros; apply (Lt_hd (mon n)); auto. simpl in |- *; unfold eqT in |- *; (intros x y p1 q1 H; rewrite H). simpl in |- *; intros; apply (Lt_tl (mon n)); auto. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)