From b30bac9e20735ab47327a2ac3122c2cfce162845 Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko
Date: Tue, 31 Jan 2023 12:46:26 -0800
Subject: Remove last sorry in Primitives

---
 tests/lean/hashmap_on_disk/Base/Primitives.lean | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'tests/lean/hashmap_on_disk/Base')

diff --git a/tests/lean/hashmap_on_disk/Base/Primitives.lean b/tests/lean/hashmap_on_disk/Base/Primitives.lean
index 71ce7153..3f1d13f1 100644
--- a/tests/lean/hashmap_on_disk/Base/Primitives.lean
+++ b/tests/lean/hashmap_on_disk/Base/Primitives.lean
@@ -1,6 +1,5 @@
 import Lean
 import Init.Data.List.Basic
-import Mathlib
 
 -------------
 -- PRELUDE --
@@ -155,12 +154,11 @@ def USize.checked_mul (n: USize) (m: USize): result USize :=
     .fail integerOverflow
 
 def USize.checked_div (n: USize) (m: USize): result USize :=
-  if h: m > 0 then
+  if m > 0 then
     .ret ⟨ n.val / m.val, by
-      simp_arith
       have h1: n.val < USize.size := n.val.isLt
       have h2: n.val.val / m.val.val <= n.val.val := @Nat.div_le_self n.val m.val
-      sorry
+      apply Nat.lt_of_le_of_lt h2 h1
     ⟩
   else
     .fail integerOverflow
-- 
cgit v1.2.3