def half_div
bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64add.bend:218
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend as W64add
import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/u32laws.bend as LW
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32half.bend as UH
218def half_div(+n: Nat) -> {C.half(n) == Nat.div(n, 2n) : Nat}:
219 Equal.trans(Nat, C.half(n), UH.hlf(n), Nat.div(n, 2n), chh(n), LW.hlf_div2(n))