no goals
m n : Nat
h : m ≤ n
⊢ ↑(n - m) = ↑n - ↑m
match m with
| 0 => rfl
| succ m =>
  show ofNat (n - succ m) = subNatNat n (succ m)
  rw [subNatNat, Nat.sub_eq_zero_of_le h]
no goals
m n : Nat
h : 0 ≤ n
⊢ ↑(n - 0) = ↑n - ↑0
rfl
m✝ n m : Nat
h : succ m ≤ n
⊢ ofNat (n - succ m) = subNatNat n (succ m)
m✝ n m : Nat
h : succ m ≤ n
⊢ ↑(n - succ m) = ↑n - ↑(succ m)
show ofNat (n - succ m) = subNatNat n (succ m)
no goals
m✝ n m : Nat
h : succ m ≤ n
⊢ ofNat (n - succ m) = subNatNat n (succ m)
rw [subNatNat, Nat.sub_eq_zero_of_le h]