def odd_val

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32laws.bend:202

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend as PD

202def odd_val(+a: U32) -> {v(U32.and(a, 1)) == Nat.mod(v(a), 2n) : Nat}:
203  +e = PD.and32(1n, a, 1, {==})
204  %Equal.sym(Nat, v(a), Nat.add(v(U32.and(a, 1)), Nat.double(PD.hp32(1n, a))), e) : {v(U32.and(a, 1)) == Nat.mod(_, 2n) : Nat}
205  mod2_bit(v(U32.and(a, 1)), PD.hp32(1n, a), PD.and32_lt(1n, 1n, {==}, a, 1, {==}))