diff --git a/src/data/nat/interval.lean b/src/data/nat/interval.lean
index 96181cf439d5d..2b21651334411 100644
--- a/src/data/nat/interval.lean
+++ b/src/data/nat/interval.lean
@@ -256,3 +256,42 @@ begin
 end
 
 end finset
+
+section induction
+
+variables {P : ℕ → Prop} (h : ∀ n, P (n + 1) → P n)
+
+include h
+
+lemma nat.decreasing_induction_of_not_bdd_above (hP : ¬ bdd_above {x | P x}) (n : ℕ) : P n :=
+let ⟨m, hm, hl⟩ := not_bdd_above_iff.1 hP n in decreasing_induction h hl.le hm
+
+lemma nat.decreasing_induction_of_infinite (hP : {x | P x}.infinite) (n : ℕ) : P n :=
+nat.decreasing_induction_of_not_bdd_above h (mt bdd_above.finite hP) n
+
+lemma nat.cauchy_induction' (seed : ℕ) (hs : P seed)
+  (hi : ∀ x, seed ≤ x → P x → ∃ y, x < y ∧ P y) (n : ℕ) : P n :=
+begin
+  apply nat.decreasing_induction_of_infinite h (λ hf, _),
+  obtain ⟨m, hP, hm⟩ := hf.exists_maximal_wrt id _ ⟨seed, hs⟩,
+  obtain ⟨y, hl, hy⟩ := hi m (le_of_not_lt $ λ hl, hl.ne $ hm seed hs hl.le) hP,
+  exact hl.ne (hm y hy hl.le),
+end
+
+lemma nat.cauchy_induction (seed : ℕ) (hs : P seed) (f : ℕ → ℕ)
+  (hf : ∀ x, seed ≤ x → P x → x < f x ∧ P (f x)) (n : ℕ) : P n :=
+seed.cauchy_induction' h hs (λ x hl hx, ⟨f x, hf x hl hx⟩) n
+
+lemma nat.cauchy_induction_mul (k seed : ℕ) (hk : 1 < k) (hs : P seed.succ)
+  (hm : ∀ x, seed < x → P x → P (k * x)) (n : ℕ) : P n :=
+begin
+  apply nat.cauchy_induction h _ hs ((*) k) (λ x hl hP, ⟨_, hm x hl hP⟩),
+  convert (mul_lt_mul_right $ seed.succ_pos.trans_le hl).2 hk,
+  rw one_mul,
+end
+
+lemma nat.cauchy_induction_two_mul (seed : ℕ) (hs : P seed.succ)
+  (hm : ∀ x, seed < x → P x → P (2 * x)) (n : ℕ) : P n :=
+nat.cauchy_induction_mul h 2 seed one_lt_two hs hm n
+
+end induction
diff --git a/src/data/set/finite.lean b/src/data/set/finite.lean
index c80267273ce9d..3021f54cba4ce 100644
--- a/src/data/set/finite.lean
+++ b/src/data/set/finite.lean
@@ -1121,12 +1121,7 @@ finite.induction_on H
   (by simp only [bUnion_empty, bdd_above_empty, ball_empty_iff])
   (λ a s ha _ hs, by simp only [bUnion_insert, ball_insert_iff, bdd_above_union, hs])
 
-lemma infinite_of_not_bdd_above : ¬ bdd_above s → s.infinite :=
-begin
-  contrapose!,
-  rw not_infinite,
-  apply finite.bdd_above,
-end
+lemma infinite_of_not_bdd_above : ¬ bdd_above s → s.infinite := mt finite.bdd_above
 
 end