def shift_amt

bend-collections-laws-math@1.0.0.0 · proofs/math/random/float.bend:45

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

45# the shift of the implementation: clz - 11 = 52 - j
46def shift_amt(+j: Nat, +hj: {Nat.is_le(j, 52n) == True{} : Bool}) -> {Nat.sub(Nat.sub(63n, j), 11n) == Nat.sub(52n, j) : Nat}:
47  %Equal.sym(Nat, Nat.sub(63n, j), Nat.add(11n, Nat.sub(52n, j)), sub63(j, hj)) : {Nat.sub(_, 11n) == Nat.sub(52n, j) : Nat}
48  N.sub_zero(Nat.sub(52n, j))