proposition: Lemma bits_above_log2 : forall a n, 0<=a -> log2 a < n -> a.[n] = false.
proof: Proof. intros a n Ha H. assert (Hn : 0<=n). { transitivity (log2 a). - apply log2_nonneg. - order'. } rewrite testbit_false by trivial. rewrite div_small. { nzsimpl; order'. } split. - order. - apply log2_lt_cancel. now rewrite log2_pow2. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog