rel を追加

Examples/Rel.lean

@@ -0,0 +1,14 @@
+import Mathlib.Tactic.GCongr
+
+variable (a b c d: Nat)
+
+-- ANCHOR: first
+example (h1 : a ≤ b) (h2 : c ≤ d) : a + c ≤ b + d := by
+  rel [h1, h2]
+-- ANCHOR_END: first
+
+
+-- ANCHOR: guess
+example (x: Int) (h1 : a ≤ b) : x ^ 2 * a ≤ x ^ 2 * b := by
+  rel [h1]
+-- ANCHOR_END: guess

src/SUMMARY.md

@@ -25,6 +25,7 @@
 - [induction: 帰納法](./induction.md)
 - [intro: 含意→や全称∀を示す](./intro.md)
 - [left, right: 論理和∨を示す](./left_right.md)
+- [rel: 不等式を使う](./rel.md)
 - [rfl: 定義そのまま](./rfl.md)
 - [ring: 環の等式を示す](./ring.md)
 - [rw: 同値変形](./rw.md)

src/rel.md

@@ -0,0 +1,15 @@
+# rel
+
+needs: `import Mathlib.Tactic.GCongr`
+
+`rel` は，不等式を代入して適用し，不等式を示します．関係(relation)を示すことからその名前があるようです．
+
+```lean
+{{#include ../Examples/Rel.lean:first}}
+```
+
+`rel` は，たとえば整数 `x: Int` に対して `0 ≤ x ^ 2` であることを自動的に適用するなど, 多少の推論を行います．
+
+```lean
+{{#include ../Examples/Rel.lean:guess}}
+```