#lang pie

;; mylte : Nat -> Nat -> Nat
;; mylte Z j = 1
;; mylte (S k) Z = 0
;; mylte (S k) (S j) = mylte k j
(claim zero<=?
  (-> Nat Nat))
(define zero<=?
  (lambda (j)
      1))

(claim step-<=?
  (-> Nat (-> Nat Nat)
      (-> Nat Nat)))
(define step-<=?
  (lambda (n-1 n-1<=?)
    (lambda (j)
      (rec-Nat j
        0
        (lambda (j-1 almost_j-1)
          (n-1<=? j-1))))))

(claim <=? (-> Nat Nat Nat))
(define <=?
  (lambda (n j)
    ((rec-Nat n
      zero<=?
      step-<=?) j)))