match hk : j - i with
| ofNat k => exists k; rw [←hk, Int.sub_eq, Int.add_left_comm, Int.add_neg_self_right, Int.add_zero]
| negSucc _ => rw [hk] at h; contradiction
i j : Int
h : (j - i).NonNeg
⊢ ∃ k, j = i + ofNat k
no goals