Bitcount.half_div2: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/number/bitcount.bend as Bitcount
Lines 13-20 of bend-collections-laws-math@1.0.0.0/proofs/math/number/bitcount.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/number/bitcount.bend&start_line=13&end_line=20

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

def half_div2(+n: Nat) -> {C.half(n) == Nat.div(n, 2n) : Nat}:
  match n:
    case 0n:
      {==}
    case 1n:
      {==}
    case 2n+ +q:
      Equal.trans(Nat, 1n+C.half(q), 1n+Nat.div(q, 2n), Nat.div(2n+q, 2n), Equal.cong(Nat, Nat, t => 1n+t, C.half(q), Nat.div(q, 2n), half_div2(q)), Equal.sym(Nat, Nat.div(2n+q, 2n), 1n+Nat.div(q, 2n), N.div2_step(q)))

Uses (7):
  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.sym
  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.div
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=div2_step
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=half