Use lsr in Compact tree for consistent unsigned shift semantics
Compact.append and Compact.root used asr (arithmetic shift right)
which preserves the sign bit. Values are non-negative by construction,
but lsr matches the unsigned division semantics of the algorithm and
is consistent with verify_inclusion in proof.ml.