def half_e
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fix64.bend:300
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fix64.bend as Fix64
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/shrn.bend as SHN
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
300def half_e(+e: U32) -> {vs(U32.shr(e)) == Nat.div(vs(e), 2n) : Nat}:
301 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)))