natural-number-game

 theorem succ_inj' {a b : mynat} (hs : succ(a) = succ(b)) :  a = b := 
 begin
   apply succ_inj,
   exact hs,
 end
 
 theorem succ_succ_inj {a b : mynat} 
                       (h : succ(succ(a)) = succ(succ(b))) : a = b := 
 begin
   apply succ_inj,
   apply succ_inj,
   exact h,
 end
 
 theorem succ_eq_succ_of_eq {a b : mynat} : a = b → succ(a) = succ(b) :=
 begin
   intro h,
   rw h,
   refl,
 end
 
 theorem succ_eq_succ_iff (a b : mynat) : succ a = succ b ↔ a = b :=
 begin
   split,
   exact succ_inj,
   exact succ_eq_succ_of_eq,
 end
 
 theorem add_right_cancel (a t b : mynat) : a + t = b + t → a = b :=
 begin
   induction t,
   intro h,
   repeat {rw add_zero at h},
   exact h,
   intro h,
   repeat {rw add_succ at h},
   apply t_ih,
   exact succ_inj h,
 end
 
 theorem add_left_cancel (t a b : mynat) : t + a = t + b → a = b :=
 begin
   rw add_comm t,
   rw add_comm t,
   exact add_right_cancel a t b,
 end
 
 lemma eq_zero_of_add_right_eq_self {a b : mynat} : a + b = a → b = 0 :=
 begin
   intro h,
   rw ← add_zero a at h,
   rw add_assoc at h,
   rw zero_add at h,
   apply add_left_cancel a b 0,
   exact h,
 end
 
 theorem succ_ne_zero (a : mynat) : succ a ≠ 0 := 
 begin
   symmetry,
   exact zero_ne_succ a,
 end
 
 lemma add_left_eq_zero {a b : mynat} (h : a + b = 0) : b = 0 :=
 begin
   cases b with d,
   refl,
   exfalso,
   rw add_succ at h,
   apply succ_ne_zero (a + d),
   exact h,
 end
 
 lemma add_right_eq_zero {a b : mynat} : a + b = 0 → a = 0 :=
 begin
   rw add_comm,
   apply add_left_eq_zero,
 end
 
 lemma ne_succ_self (n : mynat) : n ≠ succ n :=
 begin
   intro h,
   rw succ_eq_add_one at h,
   rw ← add_zero n at h,
   rw add_assoc at h,
   rw zero_add at h,
   have p := add_left_cancel n 0 1 h,
   rw one_eq_succ_zero at p,
   apply succ_ne_zero 0,
   symmetry,
   exact p,
 end