def cm0k

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

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

454def cm0k(+w: Nat, +k: Nat, +N: Nat, +hk: {Nat.is_lt(k, 1n) == True{} : Bool}) -> {cm(w, 0n, k, N) == N : Nat}:
455  match k:
456    case 0n:
457      cm0(w, N)
458    case 1n+q:
459      Empty.absurd({cm(w, 0n, 1n+q, N) == N : Nat}, N.lt_zero_absurd(q, hk))