def fin_eq

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

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

76def fin_eq(+k: Nat, +c: Bool) -> {Nat.add(hit_acc(k, k, Bool.not(c)), b2n(c)) == 1n : Nat}:
77  match c:
78    case True{}:
79      {==}
80    case False{}:
81      %Equal.sym(Bool, Nat.is_eq(k, k), True{}, N.is_eq_refl(k)) : {Nat.add(b2n(_), 0n) == 1n : Nat}
82      {==}