;;; $Id: nat-leq.scm,v 1.1 2004/02/10 04:54:14 leavens Exp $
;;; AUTHOR: Tongjie Chen and Gary T. Leavens

(load-quietly-from-lib "sub1.scm")

(deftype nat-leq (-> (number number) boolean))
(define nat-leq
  (lambda (n1 n2)
    ;; REQUIRES: n1 and n2 are natural numbers
    ;; ENSURES: Result is #t just when n1 is less than or equal to n2
    (or (zero? n1)
	(and (not (zero? n2))
	     (nat-leq (sub1 n1) (sub1 n2))))))