proposition: Lemma bits_above_log2 : forall a n, log2 a < n -> a.[n] = false.
proof: Proof. intros a n H. rewrite testbit_false. rewrite div_small. - nzsimpl; order'. - apply log2_lt_cancel. rewrite log2_pow2; trivial using le_0_l. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog