natural-number-game

 lemma one_add_le_self (x : ℕ) : x ≤ 1 + x :=
 begin
   rw le_iff_exists_add,
   use 1,
   rw add_comm,
 end
 
 lemma le_refl (x : ℕ) : x ≤ x :=
 begin
   use 0,
   rw add_zero,
   refl,
 end
 
 theorem le_succ (a b : ℕ) : a ≤ b → a ≤ (succ b) :=
 begin
   intro h,
   cases h with c hc,
   use c + 1,
   rw add_one_eq_succ,
   rw add_succ,
   rw hc,
   refl,
 end
 
 lemma zero_le (a : ℕ) : 0 ≤ a :=
 begin
   use a,
   rw zero_add,
   refl,
 end
 
 theorem le_trans (a b c : ℕ) (hab : a ≤ b) (hbc : b ≤ c) : a ≤ c :=
 begin
   cases hab with b' hb',
   cases hbc with c' hc',
   use b' + c',
   rw ← add_assoc,
   rw ← hb',
   exact hc',
 end
 
 theorem le_antisymm (a b : ℕ) (hab : a ≤ b) (hba : b ≤ a) : a = b :=
 begin
   cases hab with c hc,
   cases hba with d hd,
   rw hd at hc,
   rw add_assoc at hc,
   symmetry at hc,
   have p := eq_zero_of_add_right_eq_self hc,
   have q := add_right_eq_zero p,
   rw hd,
   rw q,
   rw add_zero,
   refl,
 end
 
 lemma le_zero (a : ℕ) (h : a ≤ 0) : a = 0 := le_antisymm _ _ h (zero_le _)
 
 lemma succ_le_succ (a b : ℕ) (h : a ≤ b) : succ a ≤ succ b :=
 begin
   cases h with c hc,
   use c,
   rw succ_add,
   rw hc,
   refl,
 end
 
 theorem le_total (a b : ℕ) : a ≤ b ∨ b ≤ a :=
 begin
   induction b with c,
   right,
   exact zero_le a,
   cases b_ih with hac hca,
   left,
   apply le_succ,
   exact hac,
   cases hca with d hd,
   cases d with e,
   rw add_zero at hd,
   left,
   rw hd,
   rw succ_eq_add_one,
   use 1,
   refl,
   right,
   use e,
   rw succ_add,
   rw ← add_succ,
   exact hd,
 end
 
 lemma le_succ_self (a : ℕ) : a ≤ succ a :=
 begin
   use 1,
   exact succ_eq_add_one a,
 end
 
 theorem add_le_add_right {a b : ℕ} : a ≤ b → ∀ t, (a + t) ≤ (b + t) :=
 begin
   intros h t,
   cases h with c hc,
   use c,
   rw add_assoc,
   rw ← add_comm c,
   rw ← add_assoc,
   rw hc,
   refl,
 end
 
 theorem le_of_succ_le_succ (a b : ℕ) : succ a ≤ succ b → a ≤ b :=
 begin
   intro h,
   cases h with c hc,
   use c,
   rw succ_add at hc,
   apply succ_inj,
   exact hc,
 end
 
 theorem not_succ_le_self (a : ℕ) : ¬ (succ a ≤ a) :=
 begin
   intro h,
   cases h with c hc,
   rw succ_add at hc,
   rw ← add_succ at hc,
   symmetry at hc,
   apply succ_ne_zero,
   apply eq_zero_of_add_right_eq_self,
   exact hc,
 end
 
 theorem add_le_add_left {a b : ℕ} (h : a ≤ b) (t : ℕ) : t + a ≤ t + b :=
 begin
   repeat {rw add_comm t},
   exact add_le_add_right h t,
 end
 
 lemma lt_aux_one (a b : ℕ) : a ≤ b ∧ ¬ (b ≤ a) → succ a ≤ b :=
 begin
   intro h,
   have p := le_total (succ a) b,
   cases p with hab hba,
   exact hab,
   cases hba with c hc,
   cases c with d,
   use 0,
   rw add_zero,
   rw add_zero at hc,
   symmetry at hc,
   exact hc,
   exfalso,
   apply h.2,
   use d,
   apply succ_inj,
   rw add_succ at hc,
   exact hc,
 end
 
 lemma lt_aux_two (a b : ℕ) : succ a ≤ b → a ≤ b ∧ ¬ (b ≤ a) :=
 begin
   intro h,
   split,
   exact le_trans _ _ _ (le_succ_self a) h,
   intro p,
   apply not_succ_le_self b,
   exact le_trans _ _ _ (succ_le_succ _ _ p) h,
 end
 
 lemma lt_iff_succ_le (a b : ℕ) : a < b ↔ succ a ≤ b :=
 begin
   split,
   intro h,
   apply lt_aux_one,
   exact h,
   intro h,
   apply lt_aux_two,
   exact h,
 end