def fin_gt

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

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

91def fin_gt(+hi: Nat, +k: Nat, +ok: Bool, +h: {Nat.is_lt(k, hi) == True{} : Bool}) -> {Nat.add(hit_acc(hi, k, ok), 0n) == 0n : Nat}:
92  match ok:
93    case True{}:
94      %Equal.sym(Bool, Nat.is_eq(hi, k), False{}, N.is_eq_sym_false(k, hi, N.is_eq_lt(k, hi, h))) : {Nat.add(b2n(_), 0n) == 0n : Nat}
95      {==}
96    case False{}:
97      {==}