proposition: Lemma leq2le : forall a b : nat, leq nat lt a b -> a <= b.
proof: Proof. intros. destruct (Nat.le_gt_cases a b) as [Hlt|Hlt]. auto. unfold leq in H. unfold not in H. case (H Hlt). Qed.
imports: Coq(List PeanoNat Wf_nat Inverse_Image) Buchberger(Bar OpenIndGoodRel Monomials)