From 063458870f1af619e5cad2119422d159f197b9ab Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Thu, 26 Sep 2024 04:01:44 +0100 Subject: [PATCH] Update src/Init/Data/BitVec/Bitblast.lean Co-authored-by: Kim Morrison --- src/Init/Data/BitVec/Bitblast.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index b4d4abdcb571..033239f1a03e 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -681,7 +681,7 @@ theorem DivModState.toNat_shiftRight_sub_one_eq This is used when proving the correctness of the divison algorithm, where we know that `r < d`. We then want to show that `((r.shiftConcat b) - d) < d` as the loop invariant. -In arithmethic, this is the same as showing that +In arithmetic, this is the same as showing that `r * 2 + 1 - d < d`, which this theorem establishes. -/ private theorem two_mul_add_sub_lt_of_lt_of_lt_two (h : a < x) (hy : y < 2) :