m n : Nat
motive : Nat → Nat → Int → Prop
hp : ∀ (i n : Nat), motive (n + i) n ↑i
hn : ∀ (i m : Nat), motive m (m + i + 1) -[i+1]
⊢ motive m n
    (match n - m with
    | 0 => ofNat (m - n)
    | succ k => -[k+1])
m n : Nat
motive : Nat → Nat → Int → Prop
hp : ∀ (i n : Nat), motive (n + i) n ↑i
hn : ∀ (i m : Nat), motive m (m + i + 1) -[i+1]
⊢ motive m n (subNatNat m n)
unfold subNatNat
no goals
m n : Nat
motive : Nat → Nat → Int → Prop
hp : ∀ (i n : Nat), motive (n + i) n ↑i
hn : ∀ (i m : Nat), motive m (m + i + 1) -[i+1]
⊢ motive m n
    (match n - m with
    | 0 => ofNat (m - n)
    | succ k => -[k+1])
match h : n - m with
| 0 =>
  have ⟨k, h⟩ := Nat.le.dest (Nat.le_of_sub_eq_zero h)
  rw [h.symm, Nat.add_sub_cancel_left]; apply hp
| succ k =>
  rw [Nat.sub_eq_iff_eq_add (Nat.le_of_lt (Nat.lt_of_sub_eq_succ h))] at h
  rw [h, Nat.add_comm]; apply hn
m n : Nat
motive : Nat → Nat → Int → Prop
hp : ∀ (i n : Nat), motive (n + i) n ↑i
hn : ∀ (i m : Nat), motive m (m + i + 1) -[i+1]
h✝ : n - m = 0
k : Nat
h : n + k = m
⊢ motive m n
    (match 0 with
    | 0 => ofNat (m - n)
    | succ k => -[k+1])
m n : Nat
motive : Nat → Nat → Int → Prop
hp : ∀ (i n : Nat), motive (n + i) n ↑i
hn : ∀ (i m : Nat), motive m (m + i + 1) -[i+1]
h : n - m = 0
⊢ motive m n
    (match 0 with
    | 0 => ofNat (m - n)
    | succ k => -[k+1])
have ⟨k, h⟩ := Nat.le.dest (Nat.le_of_sub_eq_zero h)
m n : Nat
motive : Nat → Nat → Int → Prop
hp : ∀ (i n : Nat), motive (n + i) n ↑i
hn : ∀ (i m : Nat), motive m (m + i + 1) -[i+1]
h✝ : n - m = 0
k : Nat
h : n + k = m
⊢ motive (n + k) n
    (match 0 with
    | 0 => ofNat k
    | succ k => -[k+1])
m n : Nat
motive : Nat → Nat → Int → Prop
hp : ∀ (i n : Nat), motive (n + i) n ↑i
hn : ∀ (i m : Nat), motive m (m + i + 1) -[i+1]
h✝ : n - m = 0
k : Nat
h : n + k = m
⊢ motive m n
    (match 0 with
    | 0 => ofNat (m - n)
    | succ k => -[k+1])
rw [h.symm, Nat.add_sub_cancel_left]
no goals
m n : Nat
motive : Nat → Nat → Int → Prop
hp : ∀ (i n : Nat), motive (n + i) n ↑i
hn : ∀ (i m : Nat), motive m (m + i + 1) -[i+1]
h✝ : n - m = 0
k : Nat
h : n + k = m
⊢ motive (n + k) n
    (match 0 with
    | 0 => ofNat k
    | succ k => -[k+1])
apply hp
m n : Nat
motive : Nat → Nat → Int → Prop
hp : ∀ (i n : Nat), motive (n + i) n ↑i
hn : ∀ (i m : Nat), motive m (m + i + 1) -[i+1]
k : Nat
h : n = succ k + m
⊢ motive m n
    (match succ k with
    | 0 => ofNat (m - n)
    | succ k => -[k+1])
m n : Nat
motive : Nat → Nat → Int → Prop
hp : ∀ (i n : Nat), motive (n + i) n ↑i
hn : ∀ (i m : Nat), motive m (m + i + 1) -[i+1]
k : Nat
h : n - m = succ k
⊢ motive m n
    (match succ k with
    | 0 => ofNat (m - n)
    | succ k => -[k+1])
rw [Nat.sub_eq_iff_eq_add (Nat.le_of_lt (Nat.lt_of_sub_eq_succ h))] at h
m n : Nat
motive : Nat → Nat → Int → Prop
hp : ∀ (i n : Nat), motive (n + i) n ↑i
hn : ∀ (i m : Nat), motive m (m + i + 1) -[i+1]
k : Nat
h : n = succ k + m
⊢ motive m (m + succ k)
    (match succ k with
    | 0 => ofNat (m - (m + succ k))
    | succ k => -[k+1])
m n : Nat
motive : Nat → Nat → Int → Prop
hp : ∀ (i n : Nat), motive (n + i) n ↑i
hn : ∀ (i m : Nat), motive m (m + i + 1) -[i+1]
k : Nat
h : n = succ k + m
⊢ motive m n
    (match succ k with
    | 0 => ofNat (m - n)
    | succ k => -[k+1])
rw [h, Nat.add_comm]
no goals
m n : Nat
motive : Nat → Nat → Int → Prop
hp : ∀ (i n : Nat), motive (n + i) n ↑i
hn : ∀ (i m : Nat), motive m (m + i + 1) -[i+1]
k : Nat
h : n = succ k + m
⊢ motive m (m + succ k)
    (match succ k with
    | 0 => ofNat (m - (m + succ k))
    | succ k => -[k+1])
apply hn