From af0159c3f89028c1974f9d014c9313ab59a18b39 Mon Sep 17 00:00:00 2001
From: Kaiyu Yang <kaiyuy@caltech.edu>
Date: Sat, 16 Sep 2023 11:36:23 -0700
Subject: [PATCH] Update README.md

---
 README.md | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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
 ```