proposition: Lemma bit_log2 : forall a, 0<a -> a.[log2 a] = true.
proof: Proof. intros a Ha. assert (Ha' := log2_nonneg a). destruct (log2_spec_alt a Ha) as (r & EQ & Hr). rewrite EQ at 1. rewrite testbit_true, add_comm by trivial. rewrite <- (mul_1_l (2^log2 a)) at 1. rewrite div_add by order_nz. rewrite div_small; trivial. rewrite add_0_l. apply mod_small. split; order'. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog