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 )

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

macro_rules
| `($m + $n) => `(plus $m $n)
| `($m * $n) => `(times $m $n)

@[app_unexpander plus]
meta def unexpandPlus : Lean.PrettyPrinter.Unexpander
  | `($_ $a $b) => `($a + $b)
  | _ => throw ()

@[app_unexpander times]
meta def unexpandTimes : Lean.PrettyPrinter.Unexpander
  | `($_ $a $b) => `($a * $b)
  | _ => throw ()




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

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



theorem plus_zero ( m : ℕ ) 
: 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 : ℕ ) 
: m + n.succ = (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 : ℕ )
: m + n = 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
      
theorem plus_assoc ( m n p : ℕ )
: m + ( n + p ) = ( m + n ) + p := by
  induction m using ℕ.rec
  case zero =>
    rewrite [zero_plus, zero_plus]
    rfl
  case succ m ih =>
    rewrite [succ_plus, succ_plus, succ_plus, ih]
    rfl


theorem zero_times ( n : ℕ ) 
: ℕ.zero * n = ℕ.zero := by
  unfold times
  rfl

theorem succ_times ( m n : ℕ )
: m.succ * n = n + m * n := by
  conv => lhs ; unfold times 


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

theorem times_succ ( m n : ℕ )
: m * n.succ = m + m * n := by
  induction m using ℕ.rec
  case zero =>
    unfold plus
    unfold times
    rfl
  case succ m ih =>
    unfold times
    unfold plus
    rewrite [ih]
    apply congrArg
    rewrite [plus_assoc n m (m*n)]
    rewrite [plus_assoc m n (m*n)]
    rewrite [plus_comm m n]
    rfl

theorem times_comm ( m n : ℕ )
: m * n = n * m := by
  induction m using ℕ.rec
  case zero =>
    rewrite [zero_times, times_zero]
    rfl
  case succ m ih =>
    rewrite [succ_times, times_succ]
    rewrite [ih]
    rfl

theorem times_right_distrib ( m n p : ℕ )
: (m + n ) * p = m*p + n*p := by
  induction m using ℕ.rec
  case zero =>
    rewrite [zero_plus, zero_times, zero_plus]
    rfl
  case succ m ih =>
    rewrite [succ_plus, succ_times, succ_times]
    rewrite [ih]
    rewrite [plus_assoc p (m*p) (n*p)]
    rfl

theorem times_left_distrib ( m n p : ℕ )
: m * ( n + p ) = m*n + m*p := by
  induction m using ℕ.rec
  case zero =>
    rewrite [zero_times, zero_times, zero_plus ]
    rewrite [zero_times]
    rfl
  case succ m ih =>
    rewrite [succ_times]
    rewrite [succ_times, succ_times]
    rewrite [ih]
    rewrite [← plus_assoc n p (m*n+m*p)]
    rewrite [← plus_assoc n (m*n) (p+m*p)]
    apply congrArg
    rewrite [plus_assoc p (m*n) (m*p)]
    rewrite [plus_assoc (m*n) p (m*p)]
    rewrite [plus_comm p (m*n)]
    rfl


theorem times_assoc ( m n p : ℕ )
: m * ( n * p ) = ( m * n ) * p := by
  induction m using ℕ.rec
  case zero =>
    rewrite [zero_times, zero_times, zero_times]
    rfl
  case succ m ih =>
    rewrite [succ_times, succ_times, ih]
    rewrite [times_right_distrib n (m*n) p]
    rfl