proposition: Lemma bit_log2 : forall a, a~=0 -> a.[log2 a] = true.
proof: Proof. intros a Ha. assert (Ha' : 0 < a) by (generalize (le_0_l a); order). destruct (log2_spec_alt a Ha') as (r & EQ & (_,Hr)). rewrite EQ at 1. rewrite testbit_true, add_comm. rewrite <- (mul_1_l (2^log2 a)) at 1. rewrite div_add by order_nz. rewrite div_small by trivial. rewrite add_0_l. apply mod_small. order'. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog