def mod_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/fill.bend:27

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR

27def mod_lt(+v: Nat, +q: Nat, +hq: {Nat.is_le(1n, q) == True{} : Bool}) -> {Nat.is_lt(Nat.mod(v, q), q) == True{} : Bool}:
28  match q:
29    case 0n:
30      Empty.absurd({Nat.is_lt(Nat.mod(v, 0n), 0n) == True{} : Bool}, L.false_true(hq))
31    case 1n+ +b:
32      NR.dm_lt(b, v)