diff --git a/Examples/Induction.lean b/Examples/Induction.lean
index ed62ebd6..a3c39eba 100644
--- a/Examples/Induction.lean
+++ b/Examples/Induction.lean
@@ -41,3 +41,19 @@ example (n : Nat) : 0 < fac n := by
   · simp [fac]
     positivity
 -- ANCHOR_END: dash
+
+
+-- ANCHOR: strong
+variable (P : Nat → Prop)
+
+example (n : Nat) : P n := by
+  -- `n` についての強い帰納法で示す
+  induction' n using Nat.strong_induction_on with n ih
+
+  -- 仮定が追加される
+  guard_hyp ih : ∀ (m : ℕ), m < n → P m
+
+  match n with
+  | 0 => sorry
+  | k + 1 => sorry
+-- ANCHOR_END: strong
\ No newline at end of file
diff --git a/src/induction.md b/src/induction.md
index 3d08bdbb..14656b88 100644
--- a/src/induction.md
+++ b/src/induction.md
@@ -30,3 +30,17 @@ needs: `import Mathlib.Tactic.Cases`
 ```lean
 {{#include ../Examples/Induction.lean:dash}}
 ```
+
+## 強い帰納法
+
+時には，より強い帰納法が必要なこともあります．強い帰納法とは，たとえば
+
+* `P(0)` を示す
+* `(∀ k < n, P (k)) → P (n)` を示す
+* したがって `∀ n, P (n)` である
+
+という形式で表されるような帰納法のことです．これは超限帰納法の特別な場合です．これを使用するには，`Nat.strong_induction_on` を使って次のようにします．
+
+```lean
+{{#include ../Examples/Induction.lean:strong}}
+```
\ No newline at end of file