def cnt_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/math/random/lemire.bend:131

import Base

131# #{x < N : x n < c}
132def cnt_lt(+n: Nat, +c: Nat, N: Nat) -> Nat:
133  match N:
134    case 0n:
135      0n
136    case 1n+ +x:
137      Nat.add(cnt_lt(n, c, x), b2n(Nat.is_lt(Nat.mul(x, n), c)))