def dm_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/arith.bend:27

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_value.bend as WV

27# v mod n < n   (Mathlib Nat.mod_lt)
28def dm_lt(+bp: Nat, +v: Nat) -> {Nat.is_lt(Nat.mod(v, 1n+bp), 1n+bp) == True{} : Bool}:
29  dm_l2(bp, v, WV.go(bp, v, bp, 0n, 0n, N.add_zero(bp)))