case hp
m n k : Nat
⊢ ∀ (i n : Nat), subNatNat (n + i + k) (n + k) = ↑i

case hn
m n k : Nat
⊢ ∀ (i m : Nat), subNatNat (m + k) (m + i + 1 + k) = -[i+1]
m n k : Nat
⊢ subNatNat (m + k) (n + k) = subNatNat m n
apply subNatNat_elim m n (fun m n i => subNatNat (m + k) (n + k) = i)
case hp
m n k i j : Nat
⊢ subNatNat (j + i + k) (j + k) = ↑i
case hp
m n k : Nat
⊢ ∀ (i n : Nat), subNatNat (n + i + k) (n + k) = ↑i
intro i j
case hp
m n k i j : Nat
⊢ subNatNat (j + k + i) (j + k) = ↑i
case hp
m n k i j : Nat
⊢ subNatNat (j + i + k) (j + k) = ↑i
rw [Nat.add_assoc, Nat.add_comm i k, ← Nat.add_assoc]
no goals
case hp
m n k i j : Nat
⊢ subNatNat (j + k + i) (j + k) = ↑i
exact subNatNat_add_left
case hn
m n k i j : Nat
⊢ subNatNat (j + k) (j + i + 1 + k) = -[i+1]
case hn
m n k : Nat
⊢ ∀ (i m : Nat), subNatNat (m + k) (m + i + 1 + k) = -[i+1]
intro i j
case hn
m n k i j : Nat
⊢ subNatNat (j + k) (j + k + (i + 1)) = -[i+1]
case hn
m n k i j : Nat
⊢ subNatNat (j + k) (j + i + 1 + k) = -[i+1]
rw [Nat.add_assoc j i 1, Nat.add_comm j (i+1), Nat.add_assoc, Nat.add_comm (i+1) (j+k)]
no goals
case hn
m n k i j : Nat
⊢ subNatNat (j + k) (j + k + (i + 1)) = -[i+1]
exact subNatNat_add_right