m n : Nat
⊢ toNat (subNatNat m n) = m - n
m n : Nat
⊢ toNat (↑m - ↑n) = m - n
rw [← Int.subNatNat_eq_coe]
case refine_1
m n✝ i n : Nat
⊢ (fun m n i => toNat i = m - n) (n + i) n ↑i

case refine_2
m n✝ i n : Nat
⊢ (fun m n i => toNat i = m - n) n (n + i + 1) -[i+1]
m n : Nat
⊢ toNat (subNatNat m n) = m - n
refine subNatNat_elim m n (fun m n i => toNat i = m - n) (fun i n => ?_) (fun i n => ?_)
no goals
case refine_1
m n✝ i n : Nat
⊢ (fun m n i => toNat i = m - n) (n + i) n ↑i
exact (Nat.add_sub_cancel_left ..).symm
case refine_2
m n✝ i n : Nat
⊢ toNat -[i+1] = n - (n + i + 1)
case refine_2
m n✝ i n : Nat
⊢ (fun m n i => toNat i = m - n) n (n + i + 1) -[i+1]
dsimp
case refine_2
m n✝ i n : Nat
⊢ toNat -[i+1] = 0
case refine_2
m n✝ i n : Nat
⊢ toNat -[i+1] = n - (n + i + 1)
rw [Nat.add_assoc, Nat.sub_eq_zero_of_le (Nat.le_add_right ..)]
no goals
case refine_2
m n✝ i n : Nat
⊢ toNat -[i+1] = 0
rfl