add1+=+add1.rkt

#lang pie

(claim + (-> Nat Nat Nat))

(define +
  (lambda (n j)
    (iter-Nat n
      j
      (lambda (n-1)
        (add1 n-1)))))


(claim add1+=+add1
       (Pi ((n Nat)
            (j Nat))
           (= Nat
              (add1 (+ n j))
              (+ n (add1 j)))))

(claim mot-add1+=+add1
       (-> Nat Nat U))

(define mot-add1+=+add1
  (lambda (j k)
    (= Nat
       (add1 (+ k j))
       (+ k (add1 j)))))

(claim step-add1+=+add1
       (Pi ((j Nat)
            (n-1 Nat))
           (-> (mot-add1+=+add1 j n-1)
               (mot-add1+=+add1 j (add1 n-1)))))

; arg
;(= Nat (add1 (+ n-1 j))
;       (+ n-1 (add1 j)))
;
; result
;(= Nat (add1 (+ (add1 n-1) j))
;       (+ (add1 n-1) (add1 j))))
;
;(= Nat (add1 (add1 (+ n-1 j)))
;       (add1 (+ n-1 (add1 j))))

(define step-add1+=+add1
  (lambda (j n-1)
    (lambda (add1+=+add1-n-1)
      (cong add1+=+add1-n-1 (+ 1)))))

(define add1+=+add1
  (lambda (n j)
    (ind-Nat n
             (mot-add1+=+add1 j)
             (same (add1 j))
             (step-add1+=+add1 j))))

(add1+=+add1 n-1 n-1)