diff --git a/Examples/Suffices.lean b/Examples/Suffices.lean
index 9d7fbb46..0eef4c55 100644
--- a/Examples/Suffices.lean
+++ b/Examples/Suffices.lean
@@ -1,5 +1,10 @@
-example (hPQ: P → Q) (hQR: Q → R) (hP: P) : R := by
-  -- `Q` を示せば十分
-  suffices Q from hQR this
+import Mathlib.Data.Nat.Order.Lemmas
 
-  exact hPQ hP
\ No newline at end of file
+-- ANCHOR: first
+example : 13 ∣ (2 ^ 70 + 3 ^ 70) := by
+  -- 余りがゼロであることを示せば十分
+  suffices (2 ^ 70 + 3 ^ 70) % 13 = 0 from by
+    exact Iff.mpr (Nat.dvd_iff_div_mul_eq (2 ^ 70 + 3 ^ 70) 13) rfl
+
+  rfl
+-- ANCHOR_END: first
\ No newline at end of file
diff --git a/src/suffices.md b/src/suffices.md
index ba8e16a6..09340352 100644
--- a/src/suffices.md
+++ b/src/suffices.md
@@ -10,7 +10,7 @@
 `apply` と似ていますが，`apply` と違って「十分条件になっていること」の証明が明らかでないときにも使うことができます．
 
 ```lean
-{{#include ../Examples/Suffices.lean}}
+{{#include ../Examples/Suffices.lean:first}}
 ```
 
 `suffices Q from ...` という形式の場合は，証明を直接構成することが必要です．`suffices Q from by ...` とすると，タクティクによって証明を構成するモードになります．
\ No newline at end of file