From 9f43c0c9e36e7121a8de4bd73bf9365d04b5d2b8 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Mon, 16 Dec 2024 14:58:03 +0000 Subject: [PATCH] clean up proof --- src/Init/Data/BitVec/Lemmas.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index ecfadb7e83e5..1c2b7536ffaf 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -2586,9 +2586,10 @@ private theorem Nat.div_add_le_right {z : Nat} (h : 0 < z) (x y : Nat) : theorem msb_udiv (x y : BitVec w) : (x / y).msb = (x.msb && y == 1#w) := by cases msb_x : x.msb - · simp [msb_eq_decide] at * - have : x.toNat / y.toNat ≤ x.toNat := Nat.div_le_self .. - omega + · suffices x.toNat / y.toNat < 2 ^ (w - 1) by simpa [msb_eq_decide] + calc + x.toNat / y.toNat ≤ x.toNat := by apply Nat.div_le_self + _ < 2 ^ (w - 1) := by simpa [msb_eq_decide] using msb_x . rcases w with _|w · contradiction · have : (y == 1#_) = decide (y.toNat = 1) := by