Bits.half_lt: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/bits.bend as Bits
Lines 29-35 of bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/bits.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/bits.bend&start_line=29&end_line=35

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as R

# n / 2 < n for n > 0
def half_lt(+np: Nat) -> {Nat.is_lt(Nat.div(1n+np, 2n), 1n+np) == True{} : Bool}:
  +n = {1n+np : Nat}
  +e = Equal.trans(Bool, Nat.is_le(n, Nat.div(n, 2n)), Nat.is_le(Nat.mul(n, 2n), n), False{}, R.le_div(1n, n, n),
    Equal.trans(Bool, Nat.is_le(Nat.mul(n, 2n), n), Nat.is_le(Nat.add(n, Nat.add(n, 0n)), n), False{}, Equal.cong(Nat, Bool, z => Nat.is_le(z, n), Nat.mul(n, 2n), Nat.add(n, Nat.add(n, 0n)), A.mul_comm(n, 2n)),
      Equal.trans(Bool, Nat.is_le(Nat.add(n, Nat.add(n, 0n)), n), Nat.is_le(Nat.add(n, n), n), False{}, Equal.cong(Nat, Bool, z => Nat.is_le(Nat.add(n, z), n), Nat.add(n, 0n), n, A.add_zero(n)), add_succ_nle(n, np))))
  N.not_le_lt(n, Nat.div(n, 2n), e)

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=not_le_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&name=le_div
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/bits.bend&name=add_succ_nle