proposition: Theorem sltp_wf : well_founded sltP.
proof: Proof. Proof using os. lapply (wf_inverse_image poly (Pow _ ltM) (lex_exp _ ltM) fspoly); [ intros H'3 | idtac ]. apply wf_incl with (R2 := fun x y : poly => lex_exp _ ltM (fspoly x) (fspoly y)); auto. red in |- *; auto. apply (wf_lex_exp _ ltM); auto; apply ltM_wf with (1 := os). Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)