fix: protected Nat.add_zero

FormalMathematicsLab · Nov 17, 2022 · a92c32b · a92c32b
1 parent 7372236
commit a92c32b
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/inductive_types.md b/inductive_types.md
@@ -1275,6 +1275,7 @@ Here are some additional examples:
 
 ```lean
 # namespace Hidden
+# theorem add_zero (n : Nat) : n + 0 = n := Nat.add_zero n
 open Nat
 
 theorem zero_add (n : Nat) : 0 + n = n := by