def half_le

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/natfuel.bend:465

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

465def half_le(+j: Nat) -> {Nat.is_le(Nat.div(1n+j, 2n), j) == True{} : Bool}:
466  +h = N.le_lt_trans(j, Nat.double(j), 1n+Nat.double(j), N.double_self_le(j), N.lt_succ(Nat.double(j)))
467  N.lt_succ_le(Nat.div(1n+j, 2n), j, half_below(1n+j, 1n+j, h))