law mod_lt
import bend-mathlib@0.8.1.0/nat.bend as Natimport Base
1941# A remainder is below its positive divisor: a % (1 + b) < 1 + b.
1942law mod_lt:
1943 for a: Nat
1944 for b: Nat
1945 lt(Nat.mod(a, 1n+b), 1n+b)
import bend-mathlib@0.8.1.0/nat.bend as Natimport Base
1941# A remainder is below its positive divisor: a % (1 + b) < 1 + b.
1942law mod_lt:
1943 for a: Nat
1944 for b: Nat
1945 lt(Nat.mod(a, 1n+b), 1n+b)