diff --git a/inequality.lean b/inequality.lean
@@ -0,0 +1,179 @@
+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