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

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

# n == 2 (n / 2) + n mod 2
def half_eq(+n: Nat) -> {n == Nat.add(Nat.double(Nat.div(n, 2n)), Nat.mod(n, 2n)) : Nat}:
  %Equal.sym(Nat, Nat.double(Nat.div(n, 2n)), Nat.mul(Nat.div(n, 2n), 2n), Equal.trans(Nat, Nat.double(Nat.div(n, 2n)), Nat.mul(2n, Nat.div(n, 2n)), Nat.mul(Nat.div(n, 2n), 2n), A.double_mul(Nat.div(n, 2n)), A.mul_comm(2n, Nat.div(n, 2n)))) : {n == Nat.add(_, Nat.mod(n, 2n)) : Nat}
  R.dm_eq(1n, n)

Uses (11):
  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.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.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=double_mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend&name=dm_eq