From 36b35107a48b6641a85ba5bd65b2ff2430f8c932 Mon Sep 17 00:00:00 2001
From: damiano <adomani@gmail.com>
Date: Wed, 3 Feb 2021 23:29:31 +0000
Subject: [PATCH] feat(data/nat/factorial): additional inequalities (#6026)

I added two lemmas about factorials.  I use them in the Liouville PR #4301.
---
 src/data/nat/factorial.lean | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

diff --git a/src/data/nat/factorial.lean b/src/data/nat/factorial.lean
index 5e138b6ed93aa..24e4685668065 100644
--- a/src/data/nat/factorial.lean
+++ b/src/data/nat/factorial.lean
@@ -96,4 +96,31 @@ lemma self_le_factorial : ∀ n : ℕ, n ≤ n!
 | 0 := zero_le_one
 | (k+1) := le_mul_of_one_le_right k.zero_lt_succ.le (nat.one_le_of_lt $ nat.factorial_pos _)
 
+lemma lt_factorial_self {n : ℕ} (hi : 3 ≤ n) : n < n! :=
+begin
+  rw [← succ_pred_eq_of_pos ((zero_lt_two.trans (lt.base 2)).trans_le hi), factorial_succ],
+  exact lt_mul_of_one_lt_right ((pred n).succ_pos) ((one_lt_two.trans_le
+    (le_pred_of_lt (succ_le_iff.mp hi))).trans_le (self_le_factorial _)),
+end
+
+lemma add_factorial_lt_factorial_add {i : ℕ} (n : ℕ) (hi : 2 ≤ i) :
+  i + (n + 1)! < (i + n + 1)! :=
+begin
+  rw [factorial_succ (i + _), succ_eq_add_one, add_mul, one_mul],
+  have : i ≤ i + n := le.intro rfl,
+  exact add_lt_add_of_lt_of_le (this.trans_lt ((lt_mul_iff_one_lt_right (zero_lt_two.trans_le
+    (hi.trans this))).mpr (lt_iff_le_and_ne.mpr ⟨(i + n).factorial_pos, λ g,
+    nat.not_succ_le_self 1 ((hi.trans this).trans (factorial_eq_one.mp g.symm))⟩))) (factorial_le
+    ((le_of_eq (add_comm n 1)).trans ((add_le_add_iff_right n).mpr (one_le_two.trans hi)))),
+end
+
+lemma add_factorial_lt_factorial_add' {i n : ℕ} (hi : 2 ≤ i) (hn : 1 ≤ n) :
+  i + n! < (i + n)! :=
+begin
+  cases hn,
+  { rw factorial_one,
+    exact lt_factorial_self (succ_le_succ hi) },
+  { exact add_factorial_lt_factorial_add _ hi }
+end
+
 end nat