ℕ = ℕ is decidable

decide_nat_eq.lean

open nat

/--
 Decide whether two natural numbers are equal
 (already included in LEAN standard lib)
-/

lemma eq_iff_succ_eq {a b : ℕ} : a = b <-> a+1 = b+1 :=
begin
split,
-- ==>
assume ab_eq : a = b,
rw ab_eq,
-- <==
assume ab_eq : a.succ = b.succ,
have j : Π (n : ℕ), n = n+1-1,
    from λ (n : ℕ), eq.refl n,
rw [j a, ab_eq, <-j b],
end

theorem decide_nat_eq : Π (n m : ℕ), decidable (n = m)
| zero zero := decidable.is_true (eq.refl zero)
| nat.zero (succ x) := begin
        have h : ¬(zero = (succ x)) := begin apply nat.no_confusion, end, 
        exact decidable.is_false h,
        end
| (succ x) nat.zero := begin
        have h : ¬((succ x) = zero) := begin apply nat.no_confusion, end, 
        exact decidable.is_false h,
        end
| (nat.succ dn) (nat.succ dm) := begin 
        have h : decidable (dn = dm), from decide_nat_eq dn dm,
        rw eq_iff_succ_eq at h,
        exact h,
        end