#lang pie

(claim step-+
  (-> Nat
      Nat))
(define step-+
  (lambda (+n-1)
    (add1 +n-1)))

(claim +
  (-> Nat Nat
      Nat))
(define +
  (lambda (n j)
    (iter-Nat n
      j
      step-+)))

; definitions using '+' can occur below

(claim  one Nat)
(define one (add1 zero))
(claim  two Nat)
(define two (+ one one))
(claim  three Nat)
(define three (+ one two))
(claim  four Nat)
(define four (+ one three))
(claim  five Nat)
(define five (+ one four))