Theorem: nat_eq_or_ne (BrownCs22/Homework/Hw8.lean)

State before:
n k : ℕ
⊢ n = k ∨ n ≠ k
Tactic:
exact Decidable.eq_or_ne n k
State after:
no goals