def nib_low
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fixbits.bend:101
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbits.bend as Fixbits
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/lib/u32div.bend as UD
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixgen.bend as G
101def nib_low(+x: U32) -> {U32.to_nat(U32.mod(x, 16)) == C.low(4n, U32.to_nat(x)) : Nat}:
102 Equal.trans(Nat, U32.to_nat(U32.mod(x, 16)), Nat.mod(U32.to_nat(x), 16n), C.low(4n, U32.to_nat(x)), UD.mod_nat(x, 16, {==}), Equal.sym(Nat, C.low(4n, U32.to_nat(x)), Nat.mod(U32.to_nat(x), 16n), G.low_mod(4n, U32.to_nat(x), 15n, {==})))