Merge branch 'addition-revision' into level-rewrite

2023-08-11 17:18:47 +02:00
parent 79ebd39feb 50682613c6
commit 0a593a9071
17 changed files with 92 additions and 75 deletions
--- a/Game/MyNat/Addition.lean
+++ b/Game/MyNat/Addition.lean
@@ -17,7 +17,8 @@ instance instAdd : Add MyNat where
 `add_zero` is a `simp` lemma, because if you see `a + 0`
 you usually want to simplify it to `a`.
 -/
-@[simp] theorem add_zero (a : MyNat) : a + 0 = a := by rfl
+@[simp]
+theorem add_zero (a : MyNat) : a + 0 = a := by rfl

 /--
 If `a` and `d` are natural numbers, then `add_succ a d` is the proof that