def half_e
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fix32.bend:309
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fix32.bend as Fix32
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/math/typed/w64add.bend as WA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/shrn.bend as SHN
309def half_e(+e: U32) -> {vs(U32.shr(e)) == Nat.div(vs(e), 2n) : Nat}:
310 Equal.trans(Nat, vs(U32.shr(e)), C.half(vs(e)), Nat.div(vs(e), 2n), SHN.shrn_high(e, 1n), WA.half_div(vs(e)))