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

/-
instance : Add ℕ where
  add := plus
-/

def times : ℕ → ℕ → ℕ 
  | ℕ.zero, _ => ℕ.zero
  | ℕ.succ m, n => n + times m n

infix : 75 " * " => times

/-
instance : Mul ℕ where
  mul := times
-/




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
      
theorem plus_assoc ( m n p : ℕ )
: plus m ( plus n p ) = plus ( plus 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 : ℕ ) 
: times ℕ.zero n = ℕ.zero := by
  unfold times
  rfl

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


theorem times_zero ( m : ℕ )
: times 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 : ℕ )
: times m n.succ = m + times 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 : ℕ )
: times m n = times 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 : ℕ )
: times m ( times n p ) = times ( times 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




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

#eval f 2

theorem f_doubles ( n : ℕ ) 
: f n = n * (2:ℕ) := by
  induction n using ℕ.rec
  case zero =>
    unfold f
    unfold times
    rfl
  case succ n ih =>
    rewrite [times]
    change f n.succ = ℕ.zero.succ.succ + n*(2:ℕ)
    rewrite [succ_plus, succ_plus, zero_plus]
    rewrite [f]
    rewrite [ih]
    rfl


def g : ℕ → ℕ 
  | ℕ.zero => 0
  | ℕ.succ n => (g n) + ( (2:ℕ) * n + (1:ℕ) )

theorem two_times (n : ℕ)
: (2:ℕ)*n = n + n := by
  change ℕ.zero.succ.succ * n = n + n 
  unfold times
  unfold times
  unfold times
  rewrite [plus_zero]
  rfl

theorem binomial_square (m n : ℕ)
: (m+n)*(m+n) = m*m + (2:ℕ)*m*n + n*n := by


example : ∀ (n:ℕ), g n = n * n := by
  intro n
  induction n using ℕ.rec
  case zero =>
    rewrite [times]
    rewrite [g]
    rfl
  case succ n ih =>
    rewrite [times]
    rewrite [times_succ]
    rewrite [g]
    rewrite [ih]
    conv => rhs ; arg 1 ; change (1:ℕ) + n
    rewrite [two_times]
    simp only [plus_assoc,plus_comm]