proposition: Theorem fsltP : forall p q : poly, sltP p q -> lex_exp _ ltM (fspoly p) (fspoly q).
proof: Proof. intros p q; case p; case q; unfold lex_exp in |- *; 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)