inductive ℕ : Type where
  | zero : ℕ
  | succ : ℕ → ℕ

namespace ℕ
protected def ofNat : Nat → ℕ
  | 0          => .zero
  | Nat.succ n => .succ (ℕ.ofNat n)

@[default_instance 200]
instance (n : Nat) : OfNat ℕ n where
  ofNat := ℕ.ofNat n
end ℕ

def plus : ℕ → ℕ → ℕ 
  | ℕ.zero, n => n
  | ℕ.succ m, n => ℕ.succ ( plus m n )

infix : 65 " + " => plus

theorem zero_plus ( n : ℕ ) 
: plus ℕ.zero n = n := by
  conv => lhs ; unfold plus

theorem succ_plus ( n : ℕ )
: plus m.succ n = (plus m n).succ := by
  conv => lhs ; unfold plus

theorem plus_zero ( m : ℕ ) 
: plus m ℕ.zero = m := by
  induction m using ℕ.rec
  case zero =>
    unfold plus
    rfl
  case succ m ih =>
    unfold plus
    rewrite [ih]
    rfl

theorem plus_succ ( m n : ℕ ) 
: plus m n.succ = (plus m n).succ := by
  induction m using ℕ.rec
  case zero =>
    unfold plus
    rfl
  case succ m ih =>
    unfold plus
    rewrite [ih]
    rfl

theorem plus_comm ( m n : ℕ )
: plus m n = plus n m := by
  induction m using ℕ.rec
  case zero =>
    rewrite [zero_plus, plus_zero]
    rfl
  case succ m ih =>
    rewrite [succ_plus, plus_succ]
    rewrite [ih]
    rfl


def f : ℕ → ℕ 
  | ℕ.zero => ℕ.zero
  | ℕ.succ n => (f n).succ.succ