proposition: Lemma dec_lt : DecRel nat lt.
proof: Proof. red in |- *; intros; pattern x, y in |- *. apply nat_double_ind_set; auto with arith. intros n; case n; auto with arith. intros n m H'; case H'; auto with arith. Qed.
imports: Coq(List PeanoNat Wf_nat Inverse_Image) Buchberger(Bar OpenIndGoodRel Monomials)