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
  sorry

theorem succ_plus ( n : ℕ )
: plus m.succ n = (plus m n).succ := by
  sorry

theorem plus_zero ( m : ℕ ) 
: plus m ℕ.zero = m := by
  sorry

theorem plus_succ ( m n : ℕ ) 
: plus m n.succ = (plus m n).succ := by
  sorry

theorem plus_comm ( m n : ℕ )
: plus m n = plus n m := by
  sorry


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