Theorem: Proving the remainder after division is bounded

Stream: lean4

[David Akinfemiwa]

I'm trying to prove this over the set of integers:

a - ⌊a / b⌋ * b < b

[Kevin Buzzard]

Can you write a #mwe ? This doesn't look true to me if eg b=0 or b=-1.

[David Akinfemiwa]

Kevin Buzzard said:

Can you write a #mwe ? This doesn't look true to me if eg b=0 or b=-1.

yeah i agree it's not true if b= 0 or b=1. Initially I had b>0 but couldn't get it to work
b > 1 → a - ⌊a / b⌋ * b < b

[David Akinfemiwa]

Kevin Buzzard said:

Can you write a #mwe ? This doesn't look true to me if eg b=0 or b=-1.

Sorry, my laptop was a bit buggy before. Here's the mw

intro hb
--apply?
apply (Int.sub_floor_div_mul_lt a hb)

[Kim Morrison]

Please click through at #mwe! :-) It really helps giving answers if you follow the advice there and post a complete code block.