def internal_bound

bend-mathlib@0.8.1.0 · u32.bend:499

import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat

499def internal_bound(-s: Nat, -m: Nat, e: {Nat.pow(2n, 32n) == m : Nat}, h: MNat.lt(s, m)) -> MNat.lt(s, Nat.pow(2n, 32n)):
500  %Equal.sym(Nat, Nat.pow(2n, 32n), m, e) : MNat.lt(s, _)
501  h