def nib_ones
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fixbits.bend:104
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/spec/math/number.bend as SN
import bend-collections-laws-math@1.0.0.0/src/math/fixed.bend as F
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/natural/arith.bend as R
104def nib_ones(+x: U32) -> {F.ones4(U32.to_nat(U32.mod(x, 16))) == SN.ones(4n, U32.to_nat(x)) : Nat}:
105 +hl = Equal.trans(Bool, Nat.is_lt(U32.to_nat(U32.mod(x, 16)), 16n), Nat.is_lt(Nat.mod(U32.to_nat(x), 16n), 16n), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(t, 16n), U32.to_nat(U32.mod(x, 16)), Nat.mod(U32.to_nat(x), 16n), UD.mod_nat(x, 16, {==})), R.dm_lt(15n, U32.to_nat(x)))
106 Equal.trans(Nat, F.ones4(U32.to_nat(U32.mod(x, 16))), SN.ones(4n, U32.to_nat(U32.mod(x, 16))), SN.ones(4n, U32.to_nat(x)), ones4_eq(U32.to_nat(U32.mod(x, 16)), hl), Equal.trans(Nat, SN.ones(4n, U32.to_nat(U32.mod(x, 16))), SN.ones(4n, C.low(4n, U32.to_nat(x))), SN.ones(4n, U32.to_nat(x)), Equal.cong(Nat, Nat, t => SN.ones(4n, t), U32.to_nat(U32.mod(x, 16)), C.low(4n, U32.to_nat(x)), nib_low(x)), ones_low(4n, U32.to_nat(x))))