proposition: Lemma WFlem1 : well_founded prod_lt.
proof: Proof. Proof using wfgt. unfold prod_lt in |- *; apply wf_inverse_image with (B := A); auto. Qed.
imports: Coq(List PeanoNat Wf_nat Inverse_Image) Buchberger(Bar OpenIndGoodRel Monomials)