n✝ m n : ℕ
inst✝ : NeZero n
k : Fin n
h : k ≤ 0
⊢ 0 = ↑0
n✝ m n : ℕ
inst✝ : NeZero n
k : Fin n
h : k ≤ 0
⊢ ↑k = ↑0
rw [Nat.eq_zero_of_le_zero h]
no goals
n✝ m n : ℕ
inst✝ : NeZero n
k : Fin n
h : k ≤ 0
⊢ 0 = ↑0
rfl
n✝ m n : ℕ
inst✝ : NeZero n
⊢ 0 ≤ 0
n✝ m n : ℕ
inst✝ : NeZero n
k : Fin n
⊢ k = 0 → k ≤ 0
rintro rfl
no goals
n✝ m n : ℕ
inst✝ : NeZero n
⊢ 0 ≤ 0
exact le_refl _