suffices のコード例を，多少非自明なものに変更する

lean-ja · Oct 7, 2023 · e946162 · e946162
1 parent ad027ae
commit e946162
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 5 deletions.
diff --git 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
+-- 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
diff --git 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 ...` とすると，タクティクによって証明を構成するモードになります．