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

case hn
m n : Nat
⊢ ∀ (i m : Nat), -[i+1] = ↑m - ↑(m + i + 1)
m n : Nat
⊢ subNatNat m n = ↑m - ↑n
apply subNatNat_elim m n fun m n i => i = m - n
case hp
m n✝ i n : Nat
⊢ ↑i = ↑(n + i) - ↑n
case hp
m n : Nat
⊢ ∀ (i n : Nat), ↑i = ↑(n + i) - ↑n
intros i n
no goals
case hp
m n✝ i n : Nat
⊢ ↑i = ↑(n + i) - ↑n
rw [Int.ofNat_add, Int.sub_eq_add_neg, Int.add_assoc, Int.add_left_comm,
  Int.add_right_neg, Int.add_zero]
case hn
m n✝ i n : Nat
⊢ -[i+1] = ↑n - ↑(n + i + 1)
case hn
m n : Nat
⊢ ∀ (i m : Nat), -[i+1] = ↑m - ↑(m + i + 1)
intros i n
case hn
m n✝ i n : Nat
⊢ -↑i + -↑1 = ↑n + -↑n + -↑i + -↑1
case hn
m n✝ i n : Nat
⊢ -[i+1] = ↑n - ↑(n + i + 1)
simp only [negSucc_coe, ofNat_add, Int.sub_eq_add_neg, Int.neg_add, ← Int.add_assoc]
case hn
m n✝ i n : Nat
⊢ n ≤ n
case hn
m n✝ i n : Nat
⊢ -↑i + -↑1 = ↑n + -↑n + -↑i + -↑1
rw [← @Int.sub_eq_add_neg n, ← ofNat_sub, Nat.sub_self, ofNat_zero, Int.zero_add]
no goals
case hn
m n✝ i n : Nat
⊢ n ≤ n
apply Nat.le_refl