fact: Definition log2_spec (n0 : nat) := {l : nat & {n0 = two_power l} + {two_power l < n0 /\ n0 < two_power (S l)}}.
imports: Arith Peano_dec Constants Mult_compl Wf_nat euclid Le_lt_compl shift Compare_dec two_power