Logarithm base 2 for bounded numbers.
The resulting value is the same as that computed by Nat.log2. In particular, the result for 0 is
0.
Examples:
(8 : Fin 10).log2 = (3 : Fin 10)(7 : Fin 10).log2 = (2 : Fin 10)(4 : Fin 10).log2 = (2 : Fin 10)(3 : Fin 10).log2 = (1 : Fin 10)(1 : Fin 10).log2 = (0 : Fin 10)(0 : Fin 10).log2 = (0 : Fin 10)