proposition: Lemma bit_log2_neg : forall a, a < -1 -> a.[log2 (P (-a))] = false.
proof: Proof. intros a Ha. rewrite <- (opp_involutive a) at 1. rewrite bits_opp. - apply negb_false_iff. apply bit_log2. apply opp_lt_mono in Ha. rewrite opp_involutive in Ha. apply lt_succ_lt_pred. now rewrite <- one_succ. - apply log2_nonneg. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog