diff --git a/README.md b/README.md
index 7ddc5b9..ca451cb 100644
--- a/README.md
+++ b/README.md
@@ -139,7 +139,7 @@ def retrieve(state: str, premises: List[str], k: int) -> List[str]:
     topk = scores.topk(k).indices.tolist()
     return [premises[i] for i in topk]
 
-for p in retrieve(state, premises, k=2):
+for p in retrieve(state, premises, k=3):
     print(p, end="\n\n")
 ```
 
@@ -150,6 +150,8 @@ def <a>nat.gcd</a> : nat → nat → nat
 | (succ x) y := have y % succ x < succ x, from mod_lt _ $ succ_pos _,
                 gcd (y % succ x) (succ x)
 
+@[simp] theorem <a>nat.gcd_zero_left</a> (x : nat) : gcd 0 x = x
+
 @[simp] theorem <a>nat.mod_self</a> (n : nat) : n % n = 0
 ```