-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem subNatNat_elim (m n : Nat) (motive : Nat → Nat → Int → Prop)
    (hp : ∀ i n, motive (n + i) n i)
    (hn : ∀ i m, motive m (m + i + 1) -[i+1]) :
    motive m n (subNatNat m n)

Proof state:
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)
    | k.succ => -[k+1])

Tactic:
rw [h.symm, Nat.add_sub_cancel_left]

Result:
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
    | k.succ => -[k+1])

Proof state:
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 = k.succ + m
⊢ motive m (m + k.succ)
    (match k.succ with
    | 0 => ofNat (m - (m + k.succ))
    | k.succ => -[k+1])

Tactic:
apply hn

Result:
no goals

Proof state:
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
    | k.succ => -[k+1])

Tactic:
apply hp

Result:
no goals

Proof state:
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)

Tactic:
unfold subNatNat

Result:
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)
    | k.succ => -[k+1])

Proof state:
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 = k.succ
⊢ motive m n
    (match k.succ with
    | 0 => ofNat (m - n)
    | k.succ => -[k+1])

Tactic:
rw [Nat.sub_eq_iff_eq_add (Nat.le_of_lt (Nat.lt_of_sub_eq_succ h))] at h

Result:
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 = k.succ + m
⊢ motive m n
    (match k.succ with
    | 0 => ofNat (m - n)
    | k.succ => -[k+1])

Proof state:
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)
    | k.succ => -[k+1])

Tactic:
have ⟨k, h⟩ := Nat.le.dest (Nat.le_of_sub_eq_zero h)

Result:
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)
    | k.succ => -[k+1])

Proof state:
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)
    | k.succ => -[k+1])

Tactic:
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

Result:
no goals

Proof state:
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 = k.succ + m
⊢ motive m n
    (match k.succ with
    | 0 => ofNat (m - n)
    | k.succ => -[k+1])

Tactic:
rw [h, Nat.add_comm]

Result:
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 = k.succ + m
⊢ motive m (m + k.succ)
    (match k.succ with
    | 0 => ofNat (m - (m + k.succ))
    | k.succ => -[k+1])