proposition: Theorem wf_Co : well_founded Co.
proof: Proof. unfold Co in |- *; apply wf_lexprod. apply wf_incl. exact wf_Fl. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)