diff --git a/archive/imo/imo2019_q4.lean b/archive/imo/imo2019_q4.lean
new file mode 100644
index 0000000000000..db5eb427c78ca
--- /dev/null
+++ b/archive/imo/imo2019_q4.lean
@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2020 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+-/
+import tactic.interval_cases
+import algebra.big_operators.order
+import algebra.big_operators.enat
+import data.nat.multiplicity
+
+/-!
+# IMO 2019 Q4
+
+Find all pairs `(k, n)` of positive integers such that
+```
+  k! = (2 ^ n − 1)(2 ^ n − 2)(2 ^ n − 4)···(2 ^ n − 2 ^ (n − 1))
+```
+We show in this file that this property holds iff `(k, n) = (1, 1) ∨ (k, n) = (3, 2)`.
+
+Proof sketch:
+The idea of the proof is to count the factors of 2 on both sides. The LHS has less than `k` factors
+of 2, and the RHS has exactly `n * (n - 1) / 2` factors of 2. So we know that `n * (n - 1) / 2 < k`.
+Now for `n ≥ 6` we have `RHS < 2 ^ (n ^ 2) < (n(n-1)/2)! < k!`. We then treat the cases `n < 6`
+individually.
+-/
+
+open_locale nat big_operators
+open finset multiplicity nat (hiding zero_le prime)
+
+theorem imo2019_q4_upper_bound {k n : ℕ} (hk : k > 0)
+  (h : (k! : ℤ) = ∏ i in range n, (2 ^ n - 2 ^ i)) : n < 6 :=
+begin
+  have prime_2 : prime (2 : ℤ),
+  { exact prime_iff_prime_int.mp prime_two },
+  have h2 : n * (n - 1) / 2 < k,
+  { suffices : multiplicity 2 (k! : ℤ) = (n * (n - 1) / 2 : ℕ),
+    { rw [← enat.coe_lt_coe, ← this], change multiplicity ((2 : ℕ) : ℤ) _ < _,
+      simp_rw [int.coe_nat_multiplicity, multiplicity_two_factorial_lt hk.lt.ne.symm] },
+    rw [h, multiplicity.finset.prod prime_2, ← sum_range_id, ← sum_nat_coe_enat],
+    apply sum_congr rfl, intros i hi,
+    rw [multiplicity_sub_of_gt, multiplicity_pow_self_of_prime prime_2],
+    rwa [multiplicity_pow_self_of_prime prime_2, multiplicity_pow_self_of_prime prime_2,
+      enat.coe_lt_coe, ←mem_range] },
+  rw [←not_le], intro hn,
+  apply ne_of_lt _ h.symm,
+  suffices : (∏ i in range n, 2 ^ n : ℤ) < ↑k!,
+  { apply lt_of_le_of_lt _ this, apply prod_le_prod,
+    { intros, rw [sub_nonneg], apply pow_le_pow, norm_num, apply le_of_lt, rwa [← mem_range] },
+    { intros, apply sub_le_self, apply pow_nonneg, norm_num } },
+  suffices : 2 ^ (n * n) < (n * (n - 1) / 2)!,
+  { rw [prod_const, card_range, ← pow_mul], rw [← int.coe_nat_lt_coe_nat_iff] at this,
+    convert this.trans _, norm_cast, rwa [int.coe_nat_lt_coe_nat_iff, factorial_lt],
+    refine nat.div_pos _ (by norm_num),
+    refine le_trans _ (mul_le_mul hn (pred_le_pred hn) (zero_le _) (zero_le _)),
+    norm_num },
+  refine le_induction _ _ n hn, { norm_num },
+  intros n' hn' ih,
+  have h5 : 1 ≤ 2 * n', { linarith },
+  have : 2 ^ (2 + 2) ≤ (n' * (n' - 1) / 2).succ,
+  { change succ (6 * (6 - 1) / 2) ≤ _,
+    apply succ_le_succ, apply nat.div_le_div_right,
+    exact mul_le_mul hn' (pred_le_pred hn') (zero_le _) (zero_le _) },
+  rw [triangle_succ], apply lt_of_lt_of_le _ factorial_mul_pow_le_factorial,
+  refine lt_of_le_of_lt _ (mul_lt_mul ih (nat.pow_le_pow_of_le_left this _)
+    (pow_pos (by norm_num) _) (zero_le _)),
+  rw [← pow_mul, ← pow_add], apply pow_le_pow_of_le_right, norm_num,
+  rw [add_mul 2 2],
+  convert add_le_add_left (add_le_add_left h5 (2 * n')) (n' * n') using 1, ring
+end
+
+theorem imo2019_q4 {k n : ℕ} (hk : k > 0) (hn : n > 0) :
+  (k! : ℤ) = (∏ i in range n, (2 ^ n - 2 ^ i)) ↔ (k, n) = (1, 1) ∨ (k, n) = (3, 2) :=
+begin
+  /- The implication `←` holds. -/
+  split, swap,
+  { rintro (h|h); simp [prod.ext_iff] at h; rcases h with ⟨rfl, rfl⟩;
+    norm_num [prod_range_succ, succ_mul] },
+  intro h,
+  /- We know that n < 6. -/
+  have := imo2019_q4_upper_bound hk h,
+  interval_cases n,
+  /- n = 1 -/
+  { left, congr, norm_num at h, norm_cast at h, rw [factorial_eq_one] at h, apply antisymm h,
+    apply succ_le_of_lt hk },
+  /- n = 2 -/
+  { right, congr, norm_num [prod_range_succ] at h, norm_cast at h, rw [← factorial_inj],
+    exact h, rw [h], norm_num },
+  all_goals { exfalso, norm_num [prod_range_succ] at h, norm_cast at h, },
+  /- n = 3 -/
+  { refine monotone_factorial.ne_of_lt_of_lt_nat 5 _ _ _ h; norm_num },
+  /- n = 4 -/
+  { refine monotone_factorial.ne_of_lt_of_lt_nat 7 _ _ _ h; norm_num },
+  /- n = 5 -/
+  { refine monotone_factorial.ne_of_lt_of_lt_nat 10 _ _ _ h; norm_num },
+end
diff --git a/src/algebra/big_operators/default.lean b/src/algebra/big_operators/default.lean
index 7924b69ff6c60..1453249964cf8 100644
--- a/src/algebra/big_operators/default.lean
+++ b/src/algebra/big_operators/default.lean
@@ -6,3 +6,4 @@ import algebra.big_operators.ring
 import algebra.big_operators.pi
 import algebra.big_operators.finsupp
 import algebra.big_operators.nat_antidiagonal
+import algebra.big_operators.enat
diff --git a/src/algebra/big_operators/enat.lean b/src/algebra/big_operators/enat.lean
new file mode 100644
index 0000000000000..c1d1e9c808f10
--- /dev/null
+++ b/src/algebra/big_operators/enat.lean
@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2020 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+-/
+import algebra.big_operators.basic
+import data.nat.enat
+
+/-!
+# Big operators in `enat`
+
+A simple lemma about sums in `enat`.
+-/
+open_locale big_operators
+variables {α : Type*}
+
+namespace finset
+lemma sum_nat_coe_enat (s : finset α) (f : α → ℕ) :
+  (∑ x in s, (f x : enat)) = (∑ x  in s, f x : ℕ) :=
+(enat.coe_hom.map_sum _ _).symm
+
+end finset
diff --git a/src/data/int/basic.lean b/src/data/int/basic.lean
index 250bc5a993d62..cf7c50049b9b0 100644
--- a/src/data/int/basic.lean
+++ b/src/data/int/basic.lean
@@ -35,7 +35,7 @@ instance : comm_ring int :=
   right_distrib  := int.distrib_right,
   mul_comm       := int.mul_comm }
 
-/- Extra instances to short-circuit type class resolution -/
+/-! ### Extra instances to short-circuit type class resolution -/
 -- instance : has_sub int            := by apply_instance -- This is in core
 instance : add_comm_monoid int    := by apply_instance
 instance : add_monoid int         := by apply_instance
@@ -111,7 +111,7 @@ lemma coe_nat_succ_pos (n : ℕ) : 0 < (n.succ : ℤ) := int.coe_nat_pos.2 (succ
 @[simp, norm_cast] theorem coe_nat_abs (n : ℕ) : abs (n : ℤ) = n :=
 abs_of_nonneg (coe_nat_nonneg n)
 
-/- succ and pred -/
+/-! ### succ and pred -/
 
 /-- Immediate successor of an integer: `succ n = n + 1` -/
 def succ (a : ℤ) := a + 1
@@ -194,7 +194,7 @@ begin
       exact Hp _ (le_of_lt (add_lt_of_neg_of_le (neg_succ_lt_zero _) (le_refl _))) ih } }
 end
 
-/- nat abs -/
+/-! ### nat abs -/
 
 attribute [simp] nat_abs nat_abs_of_nat nat_abs_zero nat_abs_one
 
@@ -240,7 +240,7 @@ begin
   simpa using w₂,
 end
 
-/- /  -/
+/-! ### `/`  -/
 
 @[simp] theorem of_nat_div (m n : ℕ) : of_nat (m / n) = (of_nat m) / (of_nat n) := rfl
 
@@ -358,7 +358,7 @@ by rw [mul_comm, int.mul_div_cancel _ H]
 @[simp] protected theorem div_self {a : ℤ} (H : a ≠ 0) : a / a = 1 :=
 by have := int.mul_div_cancel 1 H; rwa one_mul at this
 
-/- mod -/
+/-! ### mod -/
 
 theorem of_nat_mod (m n : nat) : (m % n : ℤ) = of_nat (m % n) := rfl
 
@@ -513,7 +513,7 @@ begin
   rw [sub_add_cancel, ← add_mod_mod, sub_add_cancel, mod_mod]
 end
 
-/- properties of / and % -/
+/-! ### properties of `/` and `%` -/
 
 @[simp] theorem mul_div_mul_of_pos {a : ℤ} (b c : ℤ) (H : 0 < a) : a * b / (a * c) = b / c :=
 suffices ∀ (m k : ℕ) (b : ℤ), (m.succ * b / (m.succ * k) : ℤ) = b / k, from
@@ -584,7 +584,7 @@ match (n % 2), h, h₁ with
 | -[1+ a] := λ _ h₁, absurd h₁ dec_trivial
 end
 
-/- dvd -/
+/-! ### dvd -/
 
 @[norm_cast] theorem coe_nat_dvd {m n : ℕ} : (↑m : ℤ) ∣ ↑n ↔ m ∣ n :=
 ⟨λ ⟨a, ae⟩, m.eq_zero_or_pos.elim
@@ -771,7 +771,22 @@ end
 lemma dvd_of_pow_dvd {p k : ℕ} {m : ℤ} (hk : 1 ≤ k) (hpk : ↑(p^k) ∣ m) : ↑p ∣ m :=
 by rw ←pow_one p; exact pow_dvd_of_le_of_pow_dvd hk hpk
 
-/- / and ordering -/
+/-- If `n > 0` then `m` is not divisible by `n` iff it is between `n * k` and `n * (k + 1)`
+  for some `k`. -/
+lemma exists_lt_and_lt_iff_not_dvd (m : ℤ) {n : ℤ} (hn : 0 < n) :
+  (∃ k, n * k < m ∧ m < n * (k + 1)) ↔ ¬ n ∣ m :=
+begin
+  split,
+  { rintro ⟨k, h1k, h2k⟩ ⟨l, rfl⟩, rw [mul_lt_mul_left hn] at h1k h2k,
+    rw [lt_add_one_iff, ← not_lt] at h2k, exact h2k h1k },
+  { intro h, rw [dvd_iff_mod_eq_zero, ← ne.def] at h,
+    have := (mod_nonneg m hn.ne.symm).lt_of_ne h.symm,
+    simp only [← mod_add_div m n] {single_pass := tt},
+    refine ⟨m / n, lt_add_of_pos_left _ this, _⟩,
+    rw [add_comm _ (1 : ℤ), left_distrib, mul_one], exact add_lt_add_right (mod_lt_of_pos _ hn) _ }
+end
+
+/-! ### `/` and ordering -/
 
 protected theorem div_mul_le (a : ℤ) {b : ℤ} (H : b ≠ 0) : a / b * b ≤ a :=
 le_of_sub_nonneg $ by rw [mul_comm, ← mod_def]; apply mod_nonneg _ H
@@ -877,7 +892,7 @@ end
 
 @[simp] theorem neg_add_neg (m n : ℕ) : -[1+m] + -[1+n] = -[1+nat.succ(m+n)] := rfl
 
-/- to_nat -/
+/-! ### to_nat -/
 
 theorem to_nat_eq_max : ∀ (a : ℤ), (to_nat a : ℤ) = max a 0
 | (n : ℕ) := (max_eq_left (coe_zero_le n)).symm
@@ -942,7 +957,7 @@ lemma to_nat_zero_of_neg : ∀ {z : ℤ}, z < 0 → z.to_nat = 0
 | (-[1+n]) _ := rfl
 | (int.of_nat n) h := (not_le_of_gt h $ int.of_nat_nonneg n).elim
 
-/- units -/
+/-! ### units -/
 
 @[simp] theorem units_nat_abs (u : units ℤ) : nat_abs u = 1 :=
 units.ext_iff.1 $ nat.units_eq_one ⟨nat_abs u, nat_abs ↑u⁻¹,
@@ -955,7 +970,7 @@ by simpa only [units.ext_iff, units_nat_abs] using nat_abs_eq u
 lemma units_inv_eq_self (u : units ℤ) : u⁻¹ = u :=
 (units_eq_one_or u).elim (λ h, h.symm ▸ rfl) (λ h, h.symm ▸ rfl)
 
-/- bitwise ops -/
+/-! ### bitwise ops -/
 
 @[simp] lemma bodd_zero : bodd 0 = ff := rfl
 @[simp] lemma bodd_one : bodd 1 = tt := rfl
@@ -1189,7 +1204,7 @@ congr_arg coe (nat.one_shiftl _)
 
 @[simp] lemma zero_shiftr (n) : shiftr 0 n = 0 := zero_shiftl _
 
-/- Least upper bound property for integers -/
+/-! ### Least upper bound property for integers -/
 
 section classical
 open_locale classical
diff --git a/src/data/nat/basic.lean b/src/data/nat/basic.lean
index 778edd9148e99..e2f90fed2bb03 100644
--- a/src/data/nat/basic.lean
+++ b/src/data/nat/basic.lean
@@ -777,6 +777,9 @@ protected lemma div_eq_zero_iff {a b : ℕ} (hb : 0 < b) : a / b = 0 ↔ a < b :
   λ h, by rw [← nat.mul_right_inj hb, ← @add_left_cancel_iff _ _ (a % b), mod_add_div,
     mod_eq_of_lt h, mul_zero, add_zero]⟩
 
+protected lemma div_eq_zero {a b : ℕ} (hb : a < b) : a / b = 0 :=
+(nat.div_eq_zero_iff $ (zero_le a).trans_lt hb).mpr hb
+
 lemma eq_zero_of_le_div {a b : ℕ} (hb : 2 ≤ b) (h : a ≤ a / b) : a = 0 :=
 eq_zero_of_mul_le hb $
   by rw mul_comm; exact (nat.le_div_iff_mul_le' (lt_of_lt_of_le dec_trivial hb)).1 h
@@ -1202,6 +1205,19 @@ dvd_trans this hdiv
 lemma dvd_of_pow_dvd {p k m : ℕ} (hk : 1 ≤ k) (hpk : p^k ∣ m) : p ∣ m :=
 by rw ←pow_one p; exact pow_dvd_of_le_of_pow_dvd hk hpk
 
+/-- `m` is not divisible by `n` iff it is between `n * k` and `n * (k + 1)` for some `k`. -/
+lemma exists_lt_and_lt_iff_not_dvd (m : ℕ) {n : ℕ} (hn : 0 < n) :
+  (∃ k, n * k < m ∧ m < n * (k + 1)) ↔ ¬ n ∣ m :=
+begin
+  split,
+  { rintro ⟨k, h1k, h2k⟩ ⟨l, rfl⟩, rw [mul_lt_mul_left hn] at h1k h2k,
+    rw [lt_succ_iff, ← not_lt] at h2k, exact h2k h1k },
+  { intro h, rw [dvd_iff_mod_eq_zero, ← ne.def, ← pos_iff_ne_zero] at h,
+    simp only [← mod_add_div m n] {single_pass := tt},
+    refine ⟨m / n, lt_add_of_pos_left _ h, _⟩,
+    rw [add_comm _ 1, left_distrib, mul_one], exact add_lt_add_right (mod_lt _ hn) _ }
+end
+
 /-! ### `find` -/
 section find
 
diff --git a/src/data/nat/bitwise.lean b/src/data/nat/bitwise.lean
index 597fe0fdcbe6d..2299e4ee94d4b 100644
--- a/src/data/nat/bitwise.lean
+++ b/src/data/nat/bitwise.lean
@@ -35,6 +35,9 @@ namespace nat
 @[simp] lemma bit_ff : bit ff = bit0 := rfl
 @[simp] lemma bit_tt : bit tt = bit1 := rfl
 
+@[simp] lemma bit_eq_zero {n : ℕ} {b : bool} : n.bit b = 0 ↔ n = 0 ∧ b = ff :=
+by { cases b; norm_num [bit0_eq_zero, nat.bit1_ne_zero] }
+
 lemma zero_of_test_bit_eq_ff {n : ℕ} (h : ∀ i, test_bit n i = ff) : n = 0 :=
 begin
   induction n using nat.binary_rec with b n hn,
diff --git a/src/data/nat/enat.lean b/src/data/nat/enat.lean
index e098de36cb9e5..9cc2d5601335d 100644
--- a/src/data/nat/enat.lean
+++ b/src/data/nat/enat.lean
@@ -109,6 +109,9 @@ roption.ext' (iff_of_true trivial h) (λ _ _, rfl)
 lemma dom_of_le_some {x : enat} {y : ℕ} : x ≤ y → x.dom :=
 λ ⟨h, _⟩, h trivial
 
+/-- The coercion `ℕ → enat` preserves `0` and addition. -/
+def coe_hom : ℕ →+ enat := ⟨coe, enat.coe_zero, enat.coe_add⟩
+
 instance : partial_order enat :=
 { le          := (≤),
   le_refl     := λ x, ⟨id, λ _, le_refl _⟩,
@@ -127,6 +130,9 @@ lemma get_le_get {x y : enat} {hx : x.dom} {hy : y.dom} :
   x.get hx ≤ y.get hy ↔ x ≤ y :=
 by conv { to_lhs, rw [← coe_le_coe, coe_get, coe_get]}
 
+protected lemma zero_lt_one : (0 : enat) < 1 :=
+by { norm_cast, norm_num }
+
 instance semilattice_sup_bot : semilattice_sup_bot enat :=
 { sup := (⊔),
   bot := (⊥),
diff --git a/src/data/nat/multiplicity.lean b/src/data/nat/multiplicity.lean
index d9ce9b3973bfe..337bc520984e7 100644
--- a/src/data/nat/multiplicity.lean
+++ b/src/data/nat/multiplicity.lean
@@ -3,10 +3,10 @@ Copyright (c) 2019 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
-import data.nat.choose.dvd
-import data.nat.modeq
+import data.nat.bitwise
+import data.nat.parity
 import ring_theory.int.basic
-import data.finset.intervals
+import algebra.big_operators.intervals
 
 /-!
 
@@ -57,28 +57,22 @@ calc multiplicity m n = ↑(Ico 1 $ ((multiplicity m n).get (finite_nat_iff.2 
 
 namespace prime
 
-lemma multiplicity_one {p : ℕ} (hp : p.prime) :
-  multiplicity p 1 = 0 :=
-by rw [multiplicity.one_right (mt nat.is_unit_iff.mp (ne_of_gt hp.one_lt))]
+lemma multiplicity_one {p : ℕ} (hp : p.prime) : multiplicity p 1 = 0 :=
+multiplicity.one_right (prime_iff_prime.mp hp).not_unit
 
 lemma multiplicity_mul {p m n : ℕ} (hp : p.prime) :
   multiplicity p (m * n) = multiplicity p m + multiplicity p n :=
-by rw [← int.coe_nat_multiplicity, ← int.coe_nat_multiplicity,
-  ← int.coe_nat_multiplicity, int.coe_nat_mul, multiplicity.mul (nat.prime_iff_prime_int.1 hp)]
+multiplicity.mul $ prime_iff_prime.mp hp
 
 lemma multiplicity_pow {p m n : ℕ} (hp : p.prime) :
   multiplicity p (m ^ n) = n •ℕ (multiplicity p m) :=
-by induction n; simp [pow_succ', hp.multiplicity_mul, *, hp.multiplicity_one, succ_nsmul,
-  add_comm]
+multiplicity.pow $ prime_iff_prime.mp hp
 
 lemma multiplicity_self {p : ℕ} (hp : p.prime) : multiplicity p p = 1 :=
-have h₁ : ¬ is_unit (p : ℤ), from mt is_unit_int.1 (ne_of_gt hp.one_lt),
-have h₂ : (p : ℤ) ≠ 0, from int.coe_nat_ne_zero.2 hp.ne_zero,
-by rw [← int.coe_nat_multiplicity, multiplicity_self h₁ h₂]
+multiplicity_self (prime_iff_prime.mp hp).not_unit hp.ne_zero
 
 lemma multiplicity_pow_self {p n : ℕ} (hp : p.prime) : multiplicity p (p ^ n) = n :=
-by induction n; simp [hp.multiplicity_one, pow_succ', hp.multiplicity_mul, *,
-  hp.multiplicity_self, succ_eq_add_one]
+multiplicity_pow_self hp.ne_zero (prime_iff_prime.mp hp).not_unit n
 
 /-- The multiplicity of a prime in `n!` is the sum of the quotients `n / p ^ i`.
   This sum is expressed over the set `Ico 1 b` where `b` is any bound at least `n` -/
@@ -96,6 +90,41 @@ lemma multiplicity_factorial {p : ℕ} (hp : p.prime) :
   ... = (∑ i in Ico 1 b, (n + 1) / p ^ i : ℕ) :
     congr_arg coe $ finset.sum_congr rfl (by intros; simp [nat.succ_div]; congr)
 
+/-- The multiplicity of `p` in `(p(n+1))!` is one more than the sum
+  of the multiplicities of `p` in `(p * n)!` and `n + 1`. -/
+lemma multiplicity_factorial_mul_succ {n p : ℕ} (hp : p.prime) :
+  multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1 :=
+begin
+  have hp' := prime_iff_prime.mp hp,
+  have h0 : 2 ≤ p := hp.two_le,
+  have h1 : 1 ≤ p * n + 1 := le_add_left _ _,
+  have h2 : p * n + 1 ≤ p * (n + 1), linarith,
+  have h3 : p * n + 1 ≤ p * (n + 1) + 1, linarith,
+  have hm : multiplicity p (p * n)! ≠ ⊤,
+  { rw [ne.def, eq_top_iff_not_finite, not_not, finite_nat_iff],
+    exact ⟨hp.ne_one, factorial_pos _⟩ },
+  revert hm,
+  have h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), multiplicity p m = 0,
+  { intros m hm, apply multiplicity_eq_zero_of_not_dvd,
+    rw [← exists_lt_and_lt_iff_not_dvd _ (pos_iff_ne_zero.mpr hp.ne_zero)], rw [Ico.mem] at hm,
+    exact ⟨n, lt_of_succ_le hm.1, hm.2⟩ },
+  simp_rw [← prod_Ico_id_eq_factorial, multiplicity.finset.prod hp', ← sum_Ico_consecutive _ h1 h3,
+    add_assoc], intro h,
+  rw [enat.add_left_cancel_iff h, sum_Ico_succ_top h2, multiplicity.mul hp',
+    hp.multiplicity_self, sum_congr rfl h4, sum_const_zero, zero_add,
+    add_comm (1 : enat)]
+end
+
+/-- The multiplicity of `p` in `(pn)!` is `n` more than that of `n!`. -/
+lemma multiplicity_factorial_mul {n p : ℕ} (hp : p.prime) :
+  multiplicity p (p * n)! = multiplicity p n! + n :=
+begin
+  induction n with n ih,
+  { simp },
+  { simp [succ_eq_add_one, multiplicity.mul, hp, prime_iff_prime.mp hp, ih,
+      multiplicity_factorial_mul_succ, add_assoc, add_left_comm] }
+end
+
 /-- A prime power divides `n!` iff it is at most the sum of the quotients `n / p ^ i`.
   This sum is expressed over the set `Ico 1 b` where `b` is any bound at least `n` -/
 lemma pow_dvd_factorial_iff {p : ℕ} {n r b : ℕ} (hp : p.prime) (hbn : n ≤ b) :
@@ -193,4 +222,26 @@ le_antisymm
     exact multiplicity_le_multiplicity_choose_add hp _ _)
 
 end prime
+
+lemma multiplicity_two_factorial_lt : ∀ {n : ℕ} (h : n ≠ 0), multiplicity 2 n! < n :=
+begin
+  have h2 := prime_iff_prime.mp prime_two,
+  refine binary_rec _ _,
+  { contradiction },
+  { intros b n ih h,
+    by_cases hn : n = 0,
+    { subst hn, simp at h, simp [h, one_right h2.not_unit, enat.zero_lt_one] },
+    have : multiplicity 2 (2 * n)! < (2 * n : ℕ),
+    { rw [prime_two.multiplicity_factorial_mul],
+      refine (enat.add_lt_add_right (ih hn) (enat.coe_ne_top _)).trans_le _,
+      rw [two_mul], norm_cast },
+    cases b,
+    { simpa [bit0_eq_two_mul n] },
+    { suffices : multiplicity 2 (2 * n + 1) + multiplicity 2 (2 * n)! < ↑(2 * n) + 1,
+      { simpa [succ_eq_add_one, multiplicity.mul, h2, prime_two, nat.bit1_eq_succ_bit0,
+          bit0_eq_two_mul n] },
+      rw [multiplicity_eq_zero_of_not_dvd (two_not_dvd_two_mul_add_one n), zero_add],
+      refine this.trans _, exact_mod_cast lt_succ_self _ }}
+end
+
 end nat
diff --git a/src/order/basic.lean b/src/order/basic.lean
index c9f53de4e5d11..744605414421b 100644
--- a/src/order/basic.lean
+++ b/src/order/basic.lean
@@ -120,6 +120,18 @@ lemma monotone.reflect_lt {α β} [linear_order α] [preorder β] {f : α → β
   {x x' : α} (h : f x < f x') : x < x' :=
 by { rw [← not_le], intro h', apply not_le_of_lt h, exact hf h' }
 
+/-- If `f` is a monotone function from `ℕ` to a preorder such that `y` lies between `f x` and
+  `f (x + 1)`, then `y` doesn't lie in the range of `f`. -/
+lemma monotone.ne_of_lt_of_lt_nat {α} [preorder α] {f : ℕ → α} (hf : monotone f)
+  (x x' : ℕ) {y : α} (h1 : f x < y) (h2 : y < f (x + 1)) : f x' ≠ y :=
+by { rintro rfl, apply (hf.reflect_lt h1).not_le, exact nat.le_of_lt_succ (hf.reflect_lt h2) }
+
+/-- If `f` is a monotone function from `ℤ` to a preorder such that `y` lies between `f x` and
+  `f (x + 1)`, then `y` doesn't lie in the range of `f`. -/
+lemma monotone.ne_of_lt_of_lt_int {α} [preorder α] {f : ℤ → α} (hf : monotone f)
+  (x x' : ℤ) {y : α} (h1 : f x < y) (h2 : y < f (x + 1)) : f x' ≠ y :=
+by { rintro rfl, apply (hf.reflect_lt h1).not_le, exact int.le_of_lt_add_one (hf.reflect_lt h2) }
+
 end monotone
 
 /-- A function `f` is strictly monotone if `a < b` implies `f a < f b`. -/